# 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*.