Propositional Logic · First-Order Logic (Optional)

Lesson 11

Nikolai Chukhin · Alexander S. Kulikov

The system we are going to propose works for expressions in any fixed vocabulary \(\Sigma\). We shall henceforth assume that \(\Sigma\) has been fixed (but in our examples we shall use the usual assortment of familiar vocabularies). Our system starts with a countably infinite set of logical axioms. The axioms are our basic valid expressions. We need the following notation: Suppose that \(\phi\) is an expression, \(x\) a variable, and \(t\) a term. We define the substitution of \(t\) for \(x\) in \(\phi\), denoted \(\phi[x \gets t]\), to be the expression obtained by replacing each free occurrence of variable \(x\) by the term \(t\). Our set of logical axioms \(\Lambda\) contains all generalizations of the basic axioms displayed below.

  • (AX0) Any expression whose Boolean form is a tautology.

  • (AX1) Any expression of the following forms:
    • (AX1a) \(t = t\).

    • (AX1b) \((t_{1} = t_{1}' \land … \land t_{k} = t_{k}') \Rightarrow f(t_{1}, …, t_{k}) = f(t_{1}', …, t_{k}')\).

    • (AX1c) \((t_{1} = t_{1}' \land … \land t_{k} = t_{k}') \Rightarrow (R(t_{1}, …, t_{k}) \Rightarrow R(t_{1}', …, t_{k}'))\).

  • (AX2) Any expression of the form \(\forall x \ \phi \Rightarrow \phi[x \gets t]\).

  • (AX3) Any expression of the form \(\phi \Rightarrow \forall x \ \phi\), with \(x\) not free in \(\phi\).

  • (AX4) Any expression of the form \(\left( \forall x \ (\phi \Rightarrow \psi) \right) \Rightarrow \left( \forall x \ \phi \Rightarrow \forall x \ \psi \right)\).

Starting from the axioms, our system generates (“proves”) new valid expressions. In particular, consider a finite sequence of first-order expressions \(S = (\phi_{1}, \phi_{2}, …, \phi_{n})\), such that, for each expression \(\phi_{i}\) in the sequence, \(1 \leq i \leq n\), either
  • (a) \(\phi_{i} \in \Lambda\), or

  • (b) there are two expressions of the form \(\psi\), \(\psi \Rightarrow \phi\) among the expressions \(\phi_{1}, …, \phi_{i-1}\).

Then we say that \(S\) is a proof of expression \(\phi_{n}\). The expression \(\phi_{n}\) is called a first-order theorem, and we write \(\vdash \phi_{n}\) (compare with \(\models \phi_{n}\)).

As an example, we prove the symmetric property of equality \(x = y \Rightarrow y = x\).

  • \(\phi_{1} = (x = y \land x = x) \Rightarrow (x = x \Rightarrow y = x)\) is an axiom from AX1c, where \(k = 2\), \(R\) is equality, \(t_{1} = t_{2} = t_{1}' = x\), and \(t_{1}' = y\)

  • \(\phi_{2} = (x = x)\) is in axiom group AX1a

  • \(\phi_{3} = x = x \Rightarrow \left((x = y \land x = x) \Rightarrow (x = x \Rightarrow y = x)\right) \Rightarrow (x = y \Rightarrow y = x)\) is in axiom group AX0. If we denote \(a \gets (x = x), b \gets (x = y), c \gets (y = x)\), the formula becomes \[a \Rightarrow ((b \land a) \Rightarrow (a \Rightarrow c)) \Rightarrow (b \Rightarrow c).\]

  • \(\phi_{4} = \left((x = y \land x = x) \Rightarrow (x = x \Rightarrow y = x)\right) \Rightarrow (x = y \Rightarrow y = x)\) from \(\phi_{2}\) and \(\phi_{3}\)

  • \(\phi_{5} = (x = y \Rightarrow y = x)\) from \(\phi_{1}\) and \(\phi_{4}\)

Therefore, \(\vdash x = y \Rightarrow y = x\). We shall give more examples of proofs later, after we develop a methodology that will make proofs a little less tedious than this.