# Proving $\vdash \neg \neg P \to P$ in first order logic, preferrably without deduction theorem

The axiom system used is

• $$A\to B \to A$$
• $$(A \to B \to C) \to (A \to B) \to A \to C$$
• $$(\neg A \to \neg B)\to (B \to A)$$
• $$(\forall x A) \to A[t/x]$$, where $$x$$ is substitutable with $$t$$ in $$A$$.
• $$\forall x (P\to Q) \to(P \to \forall x Q)$$, where $$x$$ does not occur free in $$P$$.

And there are two inference rules, modus ponens and universal generalization:

• Infer from $$\Gamma \vdash P \to Q$$ and $$\Gamma \vdash P$$, that $$\Gamma \vdash Q$$.
• Infer from $$\Gamma \vdash P$$ that $$\Gamma \vdash \forall x P$$.

For simplicity, I define $$\Gamma \vdash_c P$$ as $$\Gamma \cup \Delta \vdash P$$, where $$\Delta$$ is a collection of formulae that can be obtained by instantiating some axiom schemes.

I already know how to prove that using the deduction theorem in propositional logic. However, the deduction theorem in first order logic puts a limit on the antecedent formula, i.e. $$\Gamma, P \vdash_c Q$$ implies $$\Gamma \vdash_c P \to Q$$ if $$P$$ is closed. If we proceed to prove $$\vdash_c \neg\neg P \to P$$ using this version of deduction theorem, we will have only proved the case where $$P$$ is closed, i.e. have no free variables.

My question is, is $$\vdash_c \neg\neg P \to P$$ provable without deduction theorem? Alternatively, is it provable in first order logic, regardless of whether $$P$$ contains free variables? How?

First, here is proof that shows $$\neg \neg P \vdash P$$:

$$\begin{array}{lll} 1&\neg \neg P & Premise\\ 2&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & Axiom \ 1\\ 3&\neg \neg \neg \neg P \to \neg \neg P & MP \ 1,2\\ 4&(\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P) & Axiom \ 3\\ 5&\neg P \to \neg \neg \neg P & MP \ 3,4\\ 6&(\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P) & Axiom \ 3\\ 7&\neg \neg P \to P& MP \ 5,6\\ 8&P & MP \ 1,7\\ \end{array}$$

And so the Deduction Theorem states that this also means that $$\vdash \neg \neg P \to P$$

OK, but now you ask: Great .. but you used the Deduction Theorem. But is it provable without the Deduction Theorem?

First, the way you phrase your question makes me think that you are mixing up rules of (or within) the logic system with theorems (like the Deduction Theorem) about that system!

To be specific: In the above formal proof, I didn't use the Deduction Theorem as a rule or inference: the Deduction Theorem was never on any line. All lines were instances of either axioms or Modus Ponens, just as it should for any formal proof in this system.

However, in the above mathematical proof I did demonstrate (using a combination of a formal proof followed by a reference to the Deduction Theorem) that $$P$$ is provable from $$\neg \neg P$$. That is, I provided a formal proof that $$P$$ is provable from $$\neg \neg P$$, and then applied the Deduction Theorem to obtain the result that $$\neg \neg P \to P$$is provable from no premises at all.

But yes, I did not provide a formal proof that actually goes from no premises at all to $$\neg \neg P \to P$$. And that is of course what you really mean when you say that you want a proof without the use of the Deduction Theorem. OK, so thanks to the Deduction Theorem we already know it is possible .. but how would we actually do this?

Well, a typical proof of the Deduction Theorem will provide you with the recipe for transforming the proof above into the one you want. The basic idea is to put $$\neg \neg P$$ in front of all the statements of the original proof. That is, we conditionalize all statements with the premise that we want to discharge. Here is what it looks like:

$$\begin{array}{lll} ...\\ &\neg \neg P \to \neg \neg P &\\ ...\\ &\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) & \\ ...\\ &\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & \\ ...\\ &\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)) & \\ ...\\ &\neg \neg P \to (\neg P \to \neg \neg \neg P) & \\ ...\\ &\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P)) & \\ ...\\ &\neg \neg P \to (\neg \neg P \to P)& \\ ...\\ &\neg \neg P \to P & \\ \end{array}$$

Interestingly, I can already tell you what the line numbers are going to be, because the transformation algorithm I am going to describe below is completely systematic:

$$\begin{array}{lll} ...\\ 5&\neg \neg P \to \neg \neg P &\\ ...\\ 8&\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) & \\ ...\\ 11&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & \\ ...\\ 14&\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)) & \\ ...\\ 17&\neg \neg P \to (\neg P \to \neg \neg \neg P) & \\ ...\\ 20&\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P)) & \\ ...\\ 23&\neg \neg P \to (\neg \neg P \to P)& \\ ...\\ 26&\neg \neg P \to P & \\ \end{array}$$

OK, so how do we fill in the missing lines?

First, the original premise $$\neg \neg P$$ that we are trying to discharge has become the tautology $$\neg \neg P \to \neg \neg P$$, and typically $$\phi \to \phi$$ is one of the first proofs (if not the first proof) you typically do when discussing these axiom systems, and it takes $$5$$ lines to do it in the new proof:

$$\begin{array}{lll} 1& (\neg \neg P \to ((P \to \neg \neg P) \to \neg \neg P) \to ((\neg \neg P \to (P \to \neg \neg P)) \to (\neg \neg P \to \neg \neg P)) & Axiom 2\\ 2& \neg \neg P \to ((P \to \neg \neg P & Axiom \ 1\\ 3&(\neg \neg P \to (P \to \neg \neg P)) \to (\neg \neg P \to \neg \neg P) & MP \ 1,2\\ 4&\neg \neg P \to (P \to \neg \neg P) & Axiom \ 1\\ 5&\neg \neg P \to \neg \neg P & MP \ 3,4\\ ...\\ 8&\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) & \\ ...\\ 11&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & \\ ...\\ 14&\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)) & \\ ...\\ 17&\neg \neg P \to (\neg P \to \neg \neg \neg P) & \\ ...\\ 20&\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P)) & \\ ...\\ 23&\neg \neg P \to (\neg \neg P \to P)& \\ ...\\ 26&\neg \neg P \to P & \\ \end{array}$$

Second, any statement in the original proof we obtained as an instance of an axiom, can be obtained in the new proof as well, and that statement can then be conditionalized using Axiom 1 (indeed, Axiom 1 serves exactly that purpose of 'conditionalization'). As an example, let me do that just for line 2 of the original proof, leading to lines 6 through 8::

$$\begin{array}{lll} 1& (\neg \neg P \to ((P \to \neg \neg P) \to \neg \neg P) \to ((\neg \neg P \to (P \to \neg \neg P)) \to (\neg \neg P \to \neg \neg P)) & Axiom 2\\ 2& \neg \neg P \to ((P \to \neg \neg P & Axiom \ 1\\ 3&(\neg \neg P \to (P \to \neg \neg P)) \to (\neg \neg P \to \neg \neg P) & MP \ 1,2\\ 4&\neg \neg P \to (P \to \neg \neg P) & Axiom \ 1\\ 5&\neg \neg P \to \neg \neg P & MP \ 3,4\\ 6&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & Axiom \ 1\\ 7&(\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) \to (\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)))& Axiom \ 1\\ 8&\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) & MP \ 6,7\\ ...\\ 11&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & \\ ...\\ 14&\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)) & \\ ...\\ 17&\neg \neg P \to (\neg P \to \neg \neg \neg P) & \\ ...\\ 20&\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P)) & \\ ...\\ 23&\neg \neg P \to (\neg \neg P \to P)& \\ ...\\ 26&\neg \neg P \to P & \\ \end{array}$$

OK, so let's do this for lines 4 and 6 of the original proof as well:

$$\begin{array}{lll} 1& (\neg \neg P \to ((P \to \neg \neg P) \to \neg \neg P) \to ((\neg \neg P \to (P \to \neg \neg P)) \to (\neg \neg P \to \neg \neg P)) & Axiom 2\\ 2& \neg \neg P \to ((P \to \neg \neg P & Axiom \ 1\\ 3&(\neg \neg P \to (P \to \neg \neg P)) \to (\neg \neg P \to \neg \neg P) & MP \ 1,2\\ 4&\neg \neg P \to (P \to \neg \neg P) & Axiom \ 1\\ 5&\neg \neg P \to \neg \neg P & MP \ 3,4\\ 6&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & Axiom \ 1\\ 7&(\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) \to (\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)))& Axiom \ 1\\ 8&\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) & MP \ 6,7\\ ...\\ 11&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & \\ 12&(\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P) & Axiom \ 3\\ 13&((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)) \to (\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)))& Axiom \ 1\\ 14&\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)) & MP \ 12, 13\\ ...\\ 17&\neg \neg P \to (\neg P \to \neg \neg \neg P) & \\ 18&(\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P) & Axiom \ 3\\ 19&((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P)) \to (\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P))) & Axiom \ 1\\ 20&\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P)) & MP \ 18, 19\\ ...\\ 23&\neg \neg P \to (\neg \neg P \to P)& \\ ...\\ 26&\neg \neg P \to P & \\ \end{array}$$

Third, and finally, we need to transform any applications of MP in the original proof to the new p[roof. For this, we use Axiom 2. Indeed, Axiom 2 can be seen as a one-line statement of a 'conditionalized Modus Ponens'. Let's see how this works. In the oerignal proof, line 3 was inferred using MP from lines 1 and 2. So, in the new proof, we want to infer line $$11$$ from lines $$5$$ and %8\$. Again, for this, we use Axiom 2. Let's just highlight those very statements so you can focus on that:

$$\begin{array}{lll} 5&\neg \neg P \to \neg \neg P & \\ 8&\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) & \\ 9&(\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P))) \to ((\neg \neg P \to \neg \neg P) \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P))&Axiom \ 2\\ 10&(\neg \neg P \to \neg \neg P) \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)& MP \ 9,8\\ 11&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & MP \ 10,5\\ \end{array}$$

See how that works? OK, now let's do the same for the other instances of MP, and we get as our final result:

$$\begin{array}{lll} 1& (\neg \neg P \to ((P \to \neg \neg P) \to \neg \neg P) \to ((\neg \neg P \to (P \to \neg \neg P)) \to (\neg \neg P \to \neg \neg P)) & Axiom 2\\ 2& \neg \neg P \to ((P \to \neg \neg P & Axiom \ 1\\ 3&(\neg \neg P \to (P \to \neg \neg P)) \to (\neg \neg P \to \neg \neg P) & MP \ 1,2\\ 4&\neg \neg P \to (P \to \neg \neg P) & Axiom \ 1\\ 5&\neg \neg P \to \neg \neg P & MP \ 3,4\\ 6&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & Axiom \ 1\\ 7&(\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) \to (\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)))& Axiom \ 1\\ 8&\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) & MP \ 6,7\\ 9&(\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P))) \to ((\neg \neg P \to \neg \neg P) \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P))&Axiom \ 2\\ 10&(\neg \neg P \to \neg \neg P) \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)& MP \ 9,8\\ 11&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & MP \ 10,5\\ 12&(\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P) & Axiom \ 3\\ 13&((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)) \to (\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)))& Axiom \ 1\\ 14&\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)) & MP \ 12, 13\\ 15&(\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P))) \to ((\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) \to (\neg \neg P \to (\neg P \to \neg \neg \neg P))&Axiom \ 2\\ 16&(\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) \to (\neg \neg P \to (\neg P \to \neg \neg \neg P))&MP \ 15,14\\ 17&\neg \neg P \to (\neg P \to \neg \neg \neg P) & MP \ 16,11\\ 18&(\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P) & Axiom \ 3\\ 19&((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P)) \to (\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P))) & Axiom \ 1\\ 20&\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P)) & MP \ 18, 19\\ 21&(\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P))) \to ((\neg \neg P \to (\neg P \to \neg \neg \neg P)) \to (\neg \neg P \to (\neg \neg P \to P))) & Axiom \ 2\\ 22&(\neg \neg P \to (\neg P \to \neg \neg \neg P)) \to (\neg \neg P \to (\neg \neg P \to P))& MP \ 21,20\\ 23&\neg \neg P \to (\neg \neg P \to P)& MP \ 22, 17\\ 24&(\neg \neg P \to (\neg \neg P \to P)) \to ((\neg \neg P \to \neg \neg P) \to (\neg \neg P \to P)) & Axiom \ 2\\ 25&(\neg \neg P \to \neg \neg P) \to (\neg \neg P \to P)& MP \ 24, 23\\ 26&\neg \neg P \to P & MP \ 25, 5\\ \end{array}$$

And there you have it! A completely formal proof!

To end, a couple of notes:

1. The systematic transformation algorithm will always work .. but often it will end up doing work that isn't really necessary. For example, we did a lot of work to get to line $$11$$, but that line is identical to line $$6$$. So, we can simplify the proof to:

$$\begin{array}{lll} 1& (\neg \neg P \to ((P \to \neg \neg P) \to \neg \neg P) \to ((\neg \neg P \to (P \to \neg \neg P)) \to (\neg \neg P \to \neg \neg P)) & Axiom 2\\ 2& \neg \neg P \to ((P \to \neg \neg P & Axiom \ 1\\ 3&(\neg \neg P \to (P \to \neg \neg P)) \to (\neg \neg P \to \neg \neg P) & MP \ 1,2\\ 4&\neg \neg P \to (P \to \neg \neg P) & Axiom \ 1\\ 5&\neg \neg P \to \neg \neg P & MP \ 3,4\\ 6&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & Axiom \ 1\\ 7&(\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P) & Axiom \ 3\\ 8&((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)) \to (\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)))& Axiom \ 1\\ 9&\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)) & MP \ 7, 8\\ 10&(\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P))) \to ((\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) \to (\neg \neg P \to (\neg P \to \neg \neg \neg P))&Axiom \ 2\\ 11&(\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) \to (\neg \neg P \to (\neg P \to \neg \neg \neg P))&MP \ 10,9\\ 12&\neg \neg P \to (\neg P \to \neg \neg \neg P) & MP \ 11,6\\ 13&(\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P) & Axiom \ 3\\ 14&((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P)) \to (\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P))) & Axiom \ 1\\ 15&\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P)) & MP \ 13, 14\\ 16&(\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P))) \to ((\neg \neg P \to (\neg P \to \neg \neg \neg P)) \to (\neg \neg P \to (\neg \neg P \to P))) & Axiom \ 2\\ 17&(\neg \neg P \to (\neg P \to \neg \neg \neg P)) \to (\neg \neg P \to (\neg \neg P \to P))& MP \ 16,15\\ 18&\neg \neg P \to (\neg \neg P \to P)& MP \ 17, 12\\ 19&(\neg \neg P \to (\neg \neg P \to P)) \to ((\neg \neg P \to \neg \neg P) \to (\neg \neg P \to P)) & Axiom \ 2\\ 20&(\neg \neg P \to \neg \neg P) \to (\neg \neg P \to P)& MP \ 19, 18\\ 21&\neg \neg P \to P & MP \ 20, 5\\ \end{array}$$

1. These formal proofs are nuts! ... even with possible simplifications .. So this is exactly why in practice we use the Deduction Theorem. Again, not as a rule of inference in an actual formal proof, but rather as theorem to mathematical prove that something is formally provable.
• Thanks very much. I was confused about the "closed" restriction on deduction theorem in first order logic. I realized that I can just go through that transformation without worrying about the closed condition after all. – Trebor May 6 '20 at 15:11
• Your answer actually enriched my understanding of the whole thing, many thanks!! – Trebor May 6 '20 at 15:11
• @Trebor You're welcome! I remember being very confused about axiom systems at the start: I didn't understand why the axioms were what they were, let alone make use of them productively. So now that I understand it better, I wanted to make sure to share that! – Bram28 May 6 '20 at 15:13