How to prove $\vdash p \to p$ using Hilbert axioms?

Question

I am curious how one would figure out a proof like this, that $\vdash p \to p$ using only axioms and rules of inference:

https://proofwiki.org/wiki/Law_of_Identity/Formulation_2/Proof_3

Posting some details below to summarize it all:

Axiom 1 is $ \vdash A \to (B \to A)$

Axiom 2 is $\vdash (A \to (B \to C)) \to ((A \to B) \to (A \to C))$

Modus ponens is $A, (A \to B) \vdash B$

So we start with an instance of axiom 2: $(p \to ((p \to p) \to p)) \to ((p \to (p \to p)) \to (p \to p))$ where $A = p$ and $B = p \to p$ and $C = p $.

And then we have an instance of axiom 1: $p \to ((p \to p) \to p)$ where $A = p$ and $B = p \to p$.

Then using modus ponens on those two gets us $(p \to (p \to p)) \to (p \to p)$.

Now we make another instance of axiom 1: $p \to (p \to p)$ where $A = p$ and $B = p$.

Using modus ponens again with our old result and this new axiom gets us $p \to p$ and we're done.

But how would we have ever known how to figure this out? Is there a systematic way or is it mostly trial and error?

Answer 1

We seek to prove $p\to p$, using only the three axiom schemas and modus ponens, so we need something that ultimately implies $(p\to p)$.

By inspection: Axiom 1 suggests $p\to(p\to p)$ . Axiom 2 suggests $(p\to(B\to p))\to((p\to B)\to (p\to p))$. Axiom 3 suggests $(\neg p\to\neg p)\to(p\to p)$ .

The second seems more helpful, but for what $B$?   It is trial and error time.

Substituting $B:=p$ and using modus ponens would give $(p\to p)\to(p\to p)$ which is not really helpful.

Substituting $B:=(p\to p)$ gives $(p\to((p\to p)\to p))\to((p\to(p\to p))\to(p\to p))$ which is rather helpful.   The rest falls into place.

$$\begin{array}{l}1. & p\to(p\to p) &\text{via Axiom }1\\2. & p\to((p\to p)\to p) &\text{via Axiom }1\\ 3. & (p\to((p\to p)\to p))\to((p\to(p\to p))\to(p\to p)) & \text{via Axiom }2\\ 4. & (p\to(p\to p))\to(p\to p) &\text{via modus ponens }2,3\\ 5. & p\to p &\text{via modus ponens }1,4 \\\blacksquare \end{array}$$

---

So trial and error is involved, but a systematic approach is needed. Pattern recognition skills are quite essential.

Answer 2

I would say it is mostly accidental that this combination of axioms works to produce $p\to p$. (In comments, Daniel Schleper pointed out a relation to combinator calculus, but it is doubtful whether that should be called an explanation, or just the same accident expressed in a different language).

In fact, it is not uncommon to present Hilbert-style systems with $A\to A$ included as an axiom because the author doesn't want to confuse students with this proof that is not particularly intuitively meaningful.

Once you do have $A\to A$ and your axioms 1 and 2, things start being easier because those three axioms are exactly what you need to prove the Deduction Theorem. From that point on, proof construction becomes more natural -- since you can now think mostly in terms of Natural Deduction rather than the pure combinatory glory of the Hilbert system.

Answer 3

But how would we have ever known how to figure this out? Is there a systematic way or is it mostly trial and error?

There exists a meta-theorem in propositional calculus, discovered by J. A. Kalman, that every theorem that can get proved by substitution and detachment can get can get proved by condensed detachment or is a substitution instance of a theorem provable by condensed detachment.

Systematically, (p$\rightarrow$p) can get derived in 2 condensed detachments. Thus, the proof could have systematically got discovered first by doing two condensed detachments, then writing out a substitution and detachment proof from using that deduction, and then pushing back all substitutions to the axioms.

The process works as follows in Polish notation.

axiom 1 CpCqp
axiom 2 CCpCqrCCpqCpr
D2.1  3 CCpqCpp
D3.1  4 Cpp

Now we'll write out a substitution and detachment proof, allowing substitution in theorems:

axiom  1 CpCqp
axiom  2 CCpCqrCCpqCpr
from 2 3 CCpCqpCCpqCpp
{3, 1} 4 CCpqCpp
from 4 5 CCpCqpCpp
{5, 1} 6 Cpp

Now we just pushback all of the substitutions to the axioms:

axiom  1 CpCqp
axiom  2 CCpCqrCCpqCpr
from 2 3 CCpCCpppCCpCppCpp
from 1 4 CpCCppp
{4, 3} 5 CCpCppCpp
from 1 6 CpCpp
{5, 6} 7 Cpp