Developing natural proofs

Natural proof systems, such as the one for propositional logic discussed here and the one for first-order logic discussed here are meant to model how mathematicians prove theorems. This is why they are called "natural" proof systems. Still, in certain situations it is not really easy to find a formal proof for a logical consequence of a set of formulas. The reason might be that the natural proof is already complex, that is, that a mathematician has a hard time to find an ordinary proof; it might also be that the set of natural proof rules available is quite restrictive.

In the following, it is explained how one might go about developing a formal proof of a simple statement, using the restrictive set of proof rules of the proof system for propositional logic discussed here.

What we want to show is $\vdash X_0 \vee \neg X_0$. By completeness of the proof system, there should be a formal proof of this, because $X_0 \vee \neg X_0$ is a tautology, that is, $\models X_0 \vee \neg X_0$.

In general, just as in real math, it is a good idea to develop the formal proof from the end, that is, we look at the goal, which is $X_0 \vee \neg X_0$. We consider every rule and ask ourselves which of these rules could possibly be used in the last step of the formal proof to derive the goal.

Clearly, of the introduction rules only $\vee$-introduction results in a disjunction. But it is also clear that we will not be able to use $\vee$-introduction in the last step of the formal proof. Because when the conclusion is $X_0 \vee \neg X_1$, then the premises are $X_0$ and $\neg X_0$. But neither one of these formulas follows from the empty set.

So we are left with the eliminiation rules as candidates for the last step in the formal proof. The only one which we can exclude right away from those is the one that eliminates $\bot$, because $\bot$ is not entailed by the empty set.

As it turns out, $\neg$-elimination can be used. That is, our formal proof will look like: \begin{array}{lll} \dots\\ \neg \neg (X_0 \vee \neg X_0)\\ X_0 \vee \neg X_0 \end{array} The next question is: how do we derive $\neg \neg (X_0 \vee \neg X_0)$ from no premises (the empty set of premises)?

Let us try to use $\neg$-introduction. This rule is applicable only if we find a formal subproof of the following form: \begin{array}{lll} \neg (X_0 \vee \neg X_0)\\ \dots\\ \bot \end{array} That we can find such a formal subproof follows from completeness: $\neg (X_0 \vee \neg X_0)$ is unsatisfiable, which means it entails $\bot$.

So, we are left with the problem of developing a formal proof of $\bot$ from $\neg (X_0 \vee \neg X_0)$. One option is to use $\bot$-introduction. Then the formal subproof could be refined as follows: \begin{array}{lll} \neg (X_0 \vee \neg X_0)\\ \dots\\ X_0 \vee \neg X_0\\ \bot \end{array}

The problem that remains is to derive $X_0 \vee \neg X_0$. A natural thing to try is to use $\vee$-introduction, which would mean the formal proof looks like \begin{array}{lll} \neg (X_0 \vee \neg X_0)\\ \dots\\ X_0\\ X_0 \vee \neg X_0\\ \bot \end{array} or like \begin{array}{lll} \neg (X_0 \vee \neg X_0)\\ \dots\\ \neg X_0\\ X_0 \vee \neg X_0\\ \bot \end{array}

Which option do we choose?—The formula $X_0$ cannot be derived by an introduction rule except if we had $\bot$, which is our goal anyway. So it might be easier to try to derive $\neg X_0$, because we can use $\neg$-introduction: \begin{array}{lll} \neg (X_0 \vee \neg X_0)\\ \qquad X_0\\ \qquad \dots\\ \qquad \bot\\ \neg X_0\\ X_0 \vee \neg X_0\\ \bot \end{array} Indentation indicates a formal subproof.

The remaining gap is now easy to fill: $\vee$-introduction gives $X_0 \vee \neg X_0$ and from this we can derive $\bot$. The full formal subproof looks like this: \begin{array}{lll} \neg (X_0 \vee \neg X_0)\\ \qquad X_0\\ \qquad X_0 \vee \neg X_0\\ \qquad \bot\\ \neg X_0\\ X_0 \vee \neg X_0\\ \bot \end{array}

Altogether, we have: \begin{array}{lll} \qquad\neg (X_0 \vee \neg X_0)\\ \qquad\qquad X_0\\ \qquad\qquad X_0 \vee \neg X_0\\ \qquad\qquad \bot\\ \qquad\neg X_0\\ \qquad X_0 \vee \neg X_0\\ \qquad\bot\\ \neg \neg (X_0 \vee \neg X_0)\\ X_0 \vee \neg X_0 \end{array}

It is now an easy exercise to annotate this formal proof with line numbers and comments about which rule is applied when:

\begin{array}{lll} 1.1 & \neg (X_0 \vee \neg X_0) & \text{assumption} \\ 1.2.1 & X_0 & \text{assumption} \\ 1.2.2 & X_0 \vee \neg X_0 & (\vee\text{i-l}) \text{ with line 1.2.1} \\ 1.2.3 & \bot & (\bot\text{i}) \text{ with lines 1.2.2 and 1.1}\\ 1.3 & \neg X_0 & (\neg\text{i}) \text{with subproof 1.2}\\ 1.4 & X_0 \vee \neg X_0 & (\vee\text{i-r}) \text{ with line 1.3}\\ 1.5 & \bot & (\bot\text{i}) \text{ with lines 1.4 and 1.1}\\ 2 & \neg \neg (X_0 \vee \neg X_0) & (\neg\text{i}) \text{ with subproof 1}\\ 3 & X_0 \vee \neg X_0 & (\neg\text{e}) \text{ with line 2} \end{array}