Introduction

Proofs in a natural proof system are supposed to resemble ordinary mathematical proofs.

Suppose $\forall x_0 (P(x_0) \rightarrow Q(x_0))$ and $\exists x_0 P(x_0)$ hold. From this, $\exists x_0 Q(x_0)$ clearly follows. A mathematical argument could go as follows.

Let $c$ be one of the elements for which the second formula holds. That is, $P$ is true for $c$. From the first formula, it follows that $Q$ is true for $c$. This means $\exists x_0 Q(x_0)$ holds.

A natural formal proof uses essentially the same arguments and looks as follows.

\begin{array}{lll} 1 & \exists x_0 P(x_0) & \text{premise}\\ 2.0 & x_1 & \text{fresh and trapped}\\ 2.1 & P(x_1) & \text{assumption}\\ 2.2 & \forall x_0 (P(x_0) \rightarrow Q(x_0)) & \text{premise}\\ 2.3 & P(x_1) \to Q(x_1) & \text{$\forall$e with 2.2} \\ 2.4 & Q(x_1) & \text{$\rightarrow$e with 2.1 and 2.3} \\ 2.5 & \exists x_0 Q(x_0) & \text{$\exists$i with 2.4 and term $x_1$} \\ 3 & \exists x_0 Q(x_0) & \text{$\exists$e with 2 and term $x_1$} \end{array}

The first thing to notice is that these proofs look, more or less, like natural proofs in propositional logic: they consist of lines composed of a line number, a formula or variable, and a justification; the line numbers indicate subproofs; the justifications formalize the mathematical reasoning.

There are a couple of things to observe:

In the formal proof, a variable, $x_1$, is used instead of the identifier $c$ used in the mathematical proof.
In the mathematical proof, a fresh name $c$ is used in order to make clear that $c$ has no relation to the objects we considered so far: an existential statement does not tell us anything about the element stipulated to exist except it exists. This is reflected in the natural formal proof by requiring that a variable is to be used in the corresponding sub proof which is not used elsewhere ("fresh and trapped").
The step from line 2.2 to line 2.3 eliminates the universal quantifier: we may replace the quantified variable by whatever we like, for instance, by the fresh variable $x_1$.
Line 2.4 is known from natural proofs in propositional logic.
Line 2.5 ends subproof 2, which established that $Q$ holds for the fresh and trapped variable $x_1$. In such a situation, we are allowed to introduce an existential quantification: the step from 2.5 to 3.

Proof rules

The proof system presented here is an extension of the natural proof system for propositional logic. This means, in particalur, that formulas are built from $\bot$, predicate formulas, and equalities using $\neg$, $\vee$, $\wedge$, $\rightarrow$, the existential, and the universal quantifier. So, in addition to the propositional part, there are equality and the quantifiers.

For the propositional part, the rules from the propositional proof system are used. For the first-order part, there are two rules each for $\doteq$, $\forall$, and $\exists$, an introduction and an elimination rule, just as in propositional logic.

\begin{array}{l|c|c} \def\arraystretch{1.5} & \text{introduction} & \text{elimination}\\ \hline \hline \doteq & \frac{}{t \doteq t} \quad (\doteq\text{i}) & \frac{t_0 \doteq t_1 \quad \varphi\{x_i \mapsto t_0\}}{\varphi\{x_i \mapsto t_1\}} \quad (\doteq\text e)\\ \hline \forall & \frac{x_i \mid \dots \varphi\{x_j \mapsto x_i\}}{\forall x_j \varphi} \quad (\forall \text i) & \frac{\forall x_i \varphi}{\varphi\{x_i \mapsto t\}} \quad (\forall\text{e})\\ \hline \exists & \frac{\varphi\{x_i \mapsto t\}}{\exists x_i \varphi} \quad (\exists \text i) & \frac{\exists x_i \varphi \quad x_j \mid \varphi\{x_i \mapsto x_j\}\dots \psi}{\psi} \quad (\exists\text e) \end{array}

In the above, $t$, $t_0$, and $t_1$ stand for terms. Three dots ($\dots$) indicate a subproof, possibly with an assumption. The vertical bar ($\mid$) is used to indicate the fresh and trapped variable. Most importantly: a rule using substitution may only be applied if there are no name clashes!

Formal proofs

Just as in propositional logic, are simply sequences of lines where each line is composed of

a line number,
a formula, and
a justification.

The only exception to this is for line number with suffix $0$: the middle part is a variable rather than a formula, corresponding to the vertical bar in the proof rules above.

Periods in the line numbers indicate subproofs.

Derivability relation

Suppose a set $\Phi$ of premises is given. A formula $\psi$ is said to be derivable from $\Phi$ if there is a proof with last line $\psi$ and such that the formulas in the lines with justification "premise" are all elements of $\Phi$, in symbols: $\Phi \vdash \varphi$.

Special notation is as follows:

$\vdash \psi$ instead of $\emptyset \vdash \psi$.
$\varphi_0, \dots, \varphi_{n-1} \vdash \psi$ instead of $\{\varphi_0, \dots, \varphi_{n-1}\} \vdash \psi$.
$\varphi \SynEquiv \psi$ for $\varphi \vdash \psi$ and $\psi \vdash \varphi$.

Soundness and completeness

The important fact about the above proof system is that every formula that can be derived from a set of formulas is entailed by it (soundness) and that every formula that is entailed by a set of formulas can be derived from it (completeness).

Theorem Let $\psi$ be a first-order formula and $\Phi$ a set of first-order formulas where $\neg, \vee, \wedge, \rightarrow, \bot$ are the only connectives and constant boolean symbols used.

Soundness.: If $\Phi \vdash \psi$, then $\Phi \models \psi$.

Completeness.: If $\Phi \models \psi$, then $\Phi \vdash \psi$.

An immediate consequence is: \begin{align} \varphi \SemEquiv \psi \qquad \text{ iff } \qquad \psi \SynEquiv \varphi \enspace. \end{align}

Exercises

Exercise Geben Sie zu folgenden Folgerungen jeweils einen kommentierten natürlichen Beweis an.

$\models\exists x_0\ \neg D(x_0)\rightarrow \neg\forall x_0\ D(x_0)$
$\left\{\forall x_1\,P(x_1),\;\neg c\doteq d\right\}\models \exists x_0\,\exists x_1\bigl((P(x_0)\wedge P(x_1))\wedge \neg x_0\doteq x_1 \bigr)$
$g(c) \doteq x_0,\; \forall x_1\, g(x_1)\doteq f(x_1) \models f(c)\doteq x_0$
$S(x_0) \rightarrow \forall x_1\; R(x_1,x_1), S(x_0) \models \forall x_1\exists x_2\; R(x_1,x_2)$

Lösung

\begin{align*} &1.1 & & \exists x_0 \neg D(x_0) && \text{Annahme}\\ &1.2.0 & & x_3 && \text{frisch und gefangen}\\ &1.2.1 & & \neg D(x_3) && \text{Annahme}\\ &1.2.2.1 & & \forall x_0\ D(x_0) && \text{Annahme}\\ &1.2.2.2 & & D(x_3) && \text{$\forall$e mit 1.2.2.1 und $\{x_0\mapsto x_3\}$}\\ &1.2.2.3 & & \bot && \text{$\bot$i mit 1.2.2.2 und 1.2.1}\\ &1.2.3 & & \neg\forall x_0\ D(x_0) && \text{$\neg$i mit 1.2.2}\\ &1.3 & & \neg\forall x_0\ D(x_0) && \text{$\exists$e mit 1.1 und 1.2}\\ &2 & & \exists x_0\ \neg D(x_0) \rightarrow \neg\forall x_0\ D(x_0) && \text{$\rightarrow$i mit 1}\\ \end{align*}
\begin{align*} &1 & & \forall x_1\ P(x_1) && \text{Voraussetzung}\\ &2 & & P(d) && \text{$\forall$e mit 1 und $\{x_1\mapsto d\}$}\\ &3 & & P(c) && \text{$\forall$e mit 1 und $\{x_1\mapsto c\}$}\\ &4 & & P(c) \wedge P(d) && \text{$\wedge$i mit 2 und 3}\\ &5 & & \neg c\doteq d && \text{Voraussetzung}\\ &6 & & P(c) \wedge P(d) \wedge \neg c\doteq d && \text{$\wedge$i mit 4 und 5}\\ &7 & & \exists x_1\ (P(c) \wedge P(x_1) \wedge \neg c\doteq x_1) && \text{$\exists$i mit $6$ und Substitution $\{x_1\mapsto d\}$}\\ &8 & & \exists x_0\ \exists x_1\ \left(P(x_0) \wedge P(x_1) \wedge \neg x_0\doteq x_1\right) && \text{$\exists$i mit $7$ und Substitution $\{x_0\mapsto c\}$}\\ \end{align*}
\begin{align*} &1 & & \forall x_1\ g(x_1)\doteq f(x_1) && \text{Voraussetzung}\\ &2 & & g(c)\doteq f(c) && \text{$\forall$e mit 1 und $\{x_1\mapsto c\}$}\\ &3 & & g(c)\doteq x_0 && \text{Voraussetzung}\\ &4 & & f(c)\doteq x_0 && \text{$\doteq$e mit 2 und 3 ($x_2\doteq x_0\sigma$) und Substitutionen $\sigma_1=\{x_2\mapsto g(c)\}$ bzw.\ $\sigma_2=\{x_2\mapsto f(c)\}$}\\ \end{align*}
\begin{array}{lll} 1 & S(x_0) & \text{Voraussetzung}\\ 2 & S(x_0) \rightarrow \forall x_1 R(x_1,x_1) & \text{Voraussetzung}\\ 3 & \forall x_1\, R(x_1,x_1) & \text{$\rightarrow$e aus 1 und 2}\\ 4.0 & x_3 & \text{frisch und gefangen}\\ 4.1 & R(x_3, x_3) & \text{$\forall$e aus 3 mit $\{x_1 \mapsto x_3\}$}\\ & {\tiny(= (R(x_3, x_2))\{x_2\mapsto x_3\} )}&\\ 4.2 & \exists x_2\, R(x_3, x_2) & \text{$\exists$i aus 4.1 mit $\{x_2 \mapsto x_3\}$}\\ & {\tiny(= (\exists x_2\, R(x_1, x_2))\{x_1\mapsto x_3\} )}&\\ 5 & \forall x_1\, \exists x_2\, R(x_1, x_2) & \text{$\forall$i aus 4 mit $\{x_1\mapsto x_3\}$} \end{array}

Exercise Im Folgenden sind kurze formale Beweise zu sehen. Geben Sie an, ob die jeweils letzte Zeile tatsächlich durch korrekte Anwendung (Namenskonflikte dürfen nicht auftreten) der angegebenen Regel entstanden ist. Begründen Sie eine nicht korrekte Anwendung durch Angabe einer geeigneten Struktur und Variablenbelegung. Dabei soll es sich um ein Modell der Voraussetzungen, aber nicht um ein Modell der Formel in der letzten Zeile handeln.

$\qquad\begin{array}[t]{rll} 1 & x_0 \doteq f(x_1) & \text{Voraussetzung}\\ 2 & \exists x_1\, S(f(x_1), x_0) & \text{Voraussetzung}\\ 3 & \exists x_1\, S(f(x_1), f(x_1)) & \text{$\doteq$e mit 1 und 2} \\ & \end{array}$
$\qquad\begin{array}[t]{rll} 1 & \forall x_5\, \exists x_2\, R(x_5,x_2) & \text{Voraussetzung}\\ 2 & \exists x_2\, R(f(x_2),x_2) & \text{$\forall$e mit 1 und $\{x_5\mapsto \dots\}$ (Substituent herausfinden!)} \\ & \end{array}$
$\qquad \begin{array}[t]{rll} 1 & \forall x_2\, R(x_2,x_2) & \text{Voraussetzung}\\ 2 & \exists x_1\, \forall x_2\, R(x_1,x_2) & \text{$\exists$i mit 1 und $\{x_1\mapsto \dots\}$ (Substituent herausfinden!)} \\ & \end{array}$

Lösung

Die Anwendung der Regel $\dot{=}\mathrm{e}$ in Zeile 3 ist nicht korrekt, da bei der Substitution $x_j\mapsto f(x_1)$ ein Namenskonflikt bezüglich der Formel $\exists x_1 S(f(x_1),x_j)$ auftritt. Die Struktur $\mathcal A$ mit \begin{align*} A&=\mathbb{N},\\ f^{\mathcal A}(x) &= x + 1,\\ S^{\mathcal A}(x,y) &= \{(x,y)\mid x = 2y \}\\ \end{align*} und der Variablenbelegung $\beta=\{x_0\mapsto 2,x_1\mapsto 1\}$ bilden ein Gegenbeispiel: Die Voraussetzungen $\mathcal A,\beta\mymodels \{x_0\doteq f(x_1),\ \exists x_1\, S(f(x_1),x_0)\}$ ist erfüllt, da $\beta(x_0) = 2 = 1+1 = \beta(x_1)+1 = f^{\mathcal A}(\beta(x_1))$ ist, und es für $\beta(x_0)=2$ die Zahl $3$ gibt, sodass $f^{\mathcal A}(3)=4=2\cdot\beta(x_0)$, sodass $\langle f^{\mathcal A}(3),\beta(x_0)\rangle\in S^{\mathcal A}$. Für die Schlussfolgerung ist $\mathcal A, \beta$ jedoch kein Modell, denn es müsste eine Zahl $z\in A$ geben, sodass $z+1=2 z + 2$. Dies gilt jedoch genau für $z=-1,$ was nicht in der Trägermenge enthalten ist..
Zunächst wurde in Zeile 2 die Regel $\forall\mathrm{e}$, also $\frac{\forall x_i \varphi}{\varphi\{x_i\mapsto t\}}$, mit der Substitution $\sigma=\{x_5\mapsto f(x_2)\}$ auf $\varphi=\exists x_2\, R(x_5,x_2)$ angewendet. Diese Anwendung ist nun nicht korrekt, da es zu einem Namenskonflikt kommt, denn $x_5\in \operatorname{scope}(x_2,\exists x_2 R(x_5,x_2))$ und $x_2\in\operatorname{vars}(\sigma(x_5))$.
Die Struktur $\mathcal A$ mit \begin{align*} A&=\mathbb{N},\\ f^{\mathcal A}(x) &= x + 1,\\ R^{\mathcal A}(x,y) &= \{(x,y)\mid x = y \}\\ \end{align*} und beliebiger Variablenbelegung $\beta$ ist ein Gegenbeispiel: Offenbar gilt $R^{\mathcal A}(x,y)$ genau dann wenn $x=y$. Damit ist die Voraussetzung erfüllt, denn zu jeder Zahl $z\in A$ gibt es $z\in A$, sodass $z=z$ also $(z,z)\in R^{\mathcal A}$. Damit die Schlussfolgerung gilt, müsste es nun aber eine Zahl $z\in A$ geben, sodass $z+1 = z$. Dann wäre jedoch $1=0$, was nicht gilt.
Zunächst wurde in Zeile 2 die Regel $\exists\mathrm{i}$, also $\frac{\varphi\{x_i\mapsto t\}}{\exists x_i\varphi},$ mit der Substitution $\sigma=\{x_1\mapsto x_2\}$ auf $\varphi=\forall x_2\, R(x_1,x_2)$ angewendet. Diese Anwendung ist jedoch nicht korrekt, da es zu einem Namenskonflikt kommt, denn $x_1\in \operatorname{scope}(x_2,\forall x_2\, R(x_1,x_2))$ und $x_2\in\operatorname{vars}(\sigma(x_1))$.
Die Struktur $\mathcal A$ mit \begin{align*} A&=\mathbb{N},\\ R^{\mathcal A}(x,y) &= \{(x,y)\mid x = y \}\\ \end{align*} und beliebiger Variablenbelegung $\beta$ ist ein Gegenbeispiel: Die Voraussetzung ist erfüllt, da $z=z$ und damit $(z,z)\in R^{\mathcal A}$ für jede Zahl $z\in A$ gilt. Zu jeder Zahl $z\in A$ gibt es nun $z+1\in A$ mit $z+1\neq z$, also $(z+1,z)\not\in R^{\mathcal A}$. Damit gibt es also kein $z\in A$, sodass für alle $z'\in A$ gilt, dass $(z,z')\in R^{\mathcal A}$, und die Schlussfolgerung ist nicht erfüllt.

Exercise Give a natural proof for $x_0 \doteq x_1\vdash x_1\doteq x_0$

Exercise Give a natural proof for $\exists x_0\,\forall x_1\, x_1 \doteq x_0\vdash \forall x_0\,\forall x_1\, x_1 \doteq x_0$

Natural proof system (first-order logic)

From Learning Logic for Computer Science

Contents