First-Order Logic Syntax
(Compare to Propositional Logic Syntax.)
First order language is a set of relation symbols and function symbols , each of which comes with arity , , which are . Function symbols of arity 0 are constants. Relation symbols of arity 0 are propositional variables.
The set denotes countably infinite set of first-order variables, which is independent of the language.
- - first-order logic formula (in language )
- - atomic formula
- - literals
- - term
- - function symbol
- - relation symbol
- - first-order variables
- , are associative
- priorities, from strongest-binding:
When in doubt, use parentheses.
Example: Consider language with , , , . Then
Often we use infix notation for relation and function symbols. In the example above, if we write and in infix notation, the formula becomes
Notation: when we write this means that and are identical formulas (with identical syntax trees). For example, , but it is not the case that .
In Isabelle theorem prover we use this
Usually we treat formulas as syntax trees and not strings.
denotes the set of free variables in the given propositional formula and can be defined recursively as follows:
If , we call a closed first-order logic formula, or sentence.