This is an old revision of the document!

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{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} \]

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 \[

  \lnot \forall x.\, \forall y. R(x,y) \land Q(x) \rightarrow Q(f(y,x)) \lor P(x)

\] denotes \[

  \lnot (\forall x.\ (\forall y. ((R(x,y) \land Q(x)) \rightarrow (Q(f(y,x)) \lor P(x)))))

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 \[

  \lnot \forall x.\, \forall y. x \mathop{R} y \land Q(x) \rightarrow Q(y \mathop{f} x) \lor P(x)

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{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}\]

If $FV(F) = \emptyset$ , we call $F$ a closed formula.