How does the following hypothesis proof work for Hilbert Proof System?

so the lecture notes specify the following 3 axioms:

H1: $A\to (B\to A)$

H2: $(A\to (B\to C))\to ((A\to B)\to (A\to C))$

H3: $(\lnot A\to B)\to ((\lnot A\to \lnot B)\to A)$

Now one of the questions states:

show that $\lnot (p\to p) \vdash p$

I understand that what I am simply required to do is choose one of the axioms above such that I can replace the A,B,C in them with components of the formula $\lnot (p\to p)$ I then have to apply Modus ponens after choosing the first 2 formulas in order to derive a smaller formula, and then repeat until I get simply p.

However my question is, is there an algorithmic way of choosing which formula to select from the H1,H2,H3 and also the way in which to substitute the components of $\lnot (p\to p)$ in the components of the chosen formula at each step.

Could somebody please walk me through how these decisions are made in the following solution:

$\vdash p\to p$

1. $(p\to ((p\to p)\to p))\to ((p\to (p\to p))\to (p\to p))$ : Formula chosen A2
2. $p\to ((p\to p)\to p)$ : Formula chosen A1
3. $(p\to (p\to p))\to (p\to p)$ : Modus ponens 1,2
4. $p\to (p\to p)$ Formula chosen A2
5. $p\to p$

Unfortunately, I haven't been able to workout $\lnot(p\to p) \vdash p$ completely, so it would be great if someone could help on that too.. however what I am thinking is, $\vdash p\to p$ is fairly easy to work with intuition, however for larger formulas, how does one go with it?

-

Working in Hilbert-style axiomatic systems tends to be a rather cumbersome affair. Their beauty is in their small size, which also helps in reasoning about them. Developing intuitive proof strategies is much easier in natural deduction style systems. That said, there are still some techniques that you can use to help develop proofs in an axiomatic system like this. It is important to understand what sort of formulae each axiom schema gives you.

• A1 gives a sort of weakening; once you know that $A$ is true, then any $B$ implies $A$.
• A2 gives you a way of decomposing an inference problem. If you're starting with $A \to (B \to C)$, then if you had $A$, you could get $B \to C$. Even if you don't have $A$, though, you still might be able to infer $A \to B$. Then, since if you had $A$, you'd have $B$ as well as $B \to C$, from which you could get $C$. A2 gives you a way to get from $A \to (B \to C)$ that if $A$ would lead you to $B$, then $A$ also leads you to $C$.
• A3 is about non-contradiction. If some formula implies both $B$ and $\lnot B$, then that formula cannot be true. A3 captures this saying, if $\lnot A$ leads to $B$ and also to $\lnot B$, then $\lnot A$ mustn't be true, so $A$ must be true.

Now, an axiomatic proof system is only concerned with symbol manipulation, so the intuitive description just mentioned does not have any real formal standing, but it might help in making a choice about which axioms to use when you are trying to construct a proof.

In constructing a proof of $p$ from the hypothesis $\lnot(p \to p)$, I started by considering that $\lnot(p \to p)$ is a contradiction (indeed, you presented a proof of $p \to p$ in your question). Since you can prove $p \to p$, you should be able to prove that

• $\lnot p \to (p \to p)$,

and since you have $\lnot(p \to p)$ as a hypothesis, you should be able to prove, without too much trouble, that

• $\lnot p \to \lnot(p \to p)$.

At this point, you should be looking at A3 and wanting to instantiate as

• $(\lnot p \to (p \to p)) \to ((\lnot p \to \lnot(p \to p)) \to p)$.

Then you can apply modus ponens to infer

• $(\lnot p \to \lnot(p \to p)) \to p$,

and then apply modus ponens again, yielding

• $p$.

That's an example of the type of intuition that you might apply to proof construction in these sorts of axiomatic systems. It gets easier with practice, but these systems really are not designed for ease of use, but rather simplicity. It often helps to consider the typical semantics of the formulae (even though the proof system can used as a pure symbol manipulation system), and to ask what the intended conclusion means, and how it relates to the meanings of the hypotheses. Sometimes syntactic considerations are important too, though. For instance, you were given a premise that has a negation sign, and only one of your axiom schemata involves a negation. That does not necessarily mean that that axiom schema is the place to start, but it is worth considering, heuristically.

-
Thank you very much, for the detailed explanation. It is quite frustrating that there is no algorithmic way of at least choosing the axioms at each stage. –  user72943 Apr 17 '13 at 9:15
The biggest problem I am facing is after choosing the axioms, I am stuck on how to choose the substitution.. But your example does help indeed. –  user72943 Apr 17 '13 at 9:17
If this solved the problem, do please accept the answer, or mark it solved. Thanks! –  Joshua Taylor Apr 17 '13 at 15:08