First-Order Logic Syntax

(Compare to Propositional Logic Syntax.)

First order language ${\cal L}$ is a set of relation symbols $R$ and function symbols $f$ , each of which comes with arity $ar(R)$ , $ar(f)$ , which are $\ge 0$ . Function symbols of arity 0 are constants. Relation symbols of arity 0 are propositional variables.

The set $V$ denotes countably infinite set of first-order variables, which is independent of the language.

$\begin{equation*} \begin{array}{rcl} F &::=& A \mid \lnot F \mid (F \land F) \mid (F \lor F) \mid (F \rightarrow F) \mid (F \leftrightarrow F) \\ & \mid & \forall x.F \mid \exists x.F \\ A & ::= & R(T,\ldots,T) \mid (T = T) \\ T & ::= & V \mid f(T,\ldots,T) \end{array} \end{equation*}$

Terminology summary:

$F$ - first-order logic formula (in language ${\cal L}$ )
$A$ - atomic formula
$A, \lnot A$ - literals
$T$ - term
$f$ - function symbol
$R$ - relation symbol
$V$ - first-order variables

Omitting parentheses:

$\land$ , $\lor$ are associative
priorities, from strongest-binding: $(\lnot)\ ;\ (\land, \lor)\ ;\ (\rightarrow, \leftrightarrow)\ ;\ (\forall, \exists)$

When in doubt, use parentheses.

Example: Consider language ${\cal L} = \{ P, Q, R, f \}$ with $ar(P) = 1$ , $ar(Q) = 1$ , $ar(R) = 2$ , $ar(f) = 2$ . Then

$\begin{equation*} \lnot \forall x.\, \forall y. R(x,y) \land Q(x) \rightarrow Q(f(y,x)) \lor P(x) \end{equation*}$

denotes

$\begin{equation*} \lnot (\forall x.\ (\forall y. ((R(x,y) \land Q(x)) \rightarrow (Q(f(y,x)) \lor P(x))))) \end{equation*}$

Often we use infix notation for relation and function symbols. In the example above, if we write $R$ and $f$ in infix notation, the formula becomes

$\begin{equation*} \lnot \forall x.\, \forall y. x \mathop{R} y \land Q(x) \rightarrow Q(y \mathop{f} x) \lor P(x) \end{equation*}$

Notation: when we write $F_1 \equiv F_2$ this means that $F_1$ and $F_2$ are identical formulas (with identical syntax trees). For example, $p \land q \equiv p \land q$ , but it is not the case that $p \land q \equiv q \land p$ .

In Isabelle theorem prover we use this

ASCII notation for First-Order Logic

Usually we treat formulas as syntax trees and not strings.

$FV$ denotes the set of free variables in the given propositional formula and can be defined recursively as follows:

$\begin{equation*}\begin{array}{rcl} FV(x) &=& \{ x \}, \mbox{ for } x \in V \\ FV(f(t_1,\ldots,t_n)) &=& F(t_1) \cup \ldots \cup F(t_n) \\ FV(R(t_1,\ldots,t_n)) &=& F(t_1) \cup \ldots \cup F(t_n) \\ FV(t_1 = t_2) &=& F(t_1) \cup F(t_2) \\ FV(\lnot F) &=& FV(F) \\ FV(F_1 \land F_2) &=& FV(F_1) \cup FV(F_2) \\ FV(F_1 \lor F_2) &=& FV(F_1) \cup FV(F_2) \\ FV(F_1 \rightarrow F_2) &=& FV(F_1) \cup FV(F_2) \\ FV(F_1 \leftrightarrow F_2) &=& FV(F_1) \cup FV(F_2) \\ FV(\forall x.F) &=& FV(F) \setminus \{x\} \\ FV(\exists x.F) &=& FV(F) \setminus \{x\} \end{array}\end{equation*}$

If $FV(F) = \emptyset$ , we call $F$ a closed first-order logic formula, or sentence.