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.

    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)  

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)


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

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

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