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.

Terminology summary:

• - first-order logic formula (in language )
• - atomic formula
• - literals
• - term
• - function symbol
• - relation symbol
• - first-order variables

Omitting parentheses:

• , are associative
• priorities, from strongest-binding:

When in doubt, use parentheses.

Example: Consider language with , , , . Then

denotes

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

ASCII notation for First-Order Logic

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.