LARA

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.