Definition. FOL - Syntax [000v]

bound: if it is within the scope of a quantifier that binds it. E.g., in \(\forall x.\ P(x, y)\), the variable \(x\) is bound.
free: if it is not bound by any quantifier within the formula. E.g., in \(\forall x.\ P(x, y)\), the variable \(y\) is free.

We can define a first order language as a tuple of 3 sets \(\langle \mathcal C, \mathcal F, \mathcal R\rangle \) where:

Constants (\(\mathcal C\)): the set of constants in the language. E.g., \(\{a, b, c\}\)
Function Symbols (\(\mathcal F\)): the set of function symbols in the language. E.g., \(\{f, g, h\}\)
Relation Symbols (\(\mathcal R\)): the set of relation symbols in the language. E.g., \(\{R, S, T\}\)

Using BNF we can define the syntax as follows

Here the atom \(p\) represents an atomic predicate applied to terms \(t_1, \ldots , t_n\), where \(p \in \mathcal R\) with an arity of \(n\)

VU-VFS-2025. Lecture 3 - First Order Logic [000u]