Finding a formal deduction from an empty set of premises

Question

I can't seem to make sense of any of this. I'm given a set of axioms schemes, modus ponens as the inference rule and I'm supposed to find a formal deduction. The question (question 1) is here. It would be greatly appreciated if someone could explain to me what these axioms mean, and how to go about solving this problem using modus ponens as I'm not sure how to apply it. Thank you

Answer 1

A3 with $\phi = p$, $\psi = q$ gives $((\lnot p) \rightarrow (\lnot q)) \rightarrow (q \rightarrow p)$.

A2 with $\phi = ((\lnot p) \rightarrow (\lnot q)), \psi = q, \chi = p$ gives $(((\lnot p) \rightarrow (\lnot q)) \rightarrow (q \rightarrow p)) \rightarrow ((((\lnot p) \rightarrow (\lnot q)) \rightarrow q ) \rightarrow ( ((\lnot p) \rightarrow (\lnot q)) \rightarrow p) )$.

Answer 2

A formal proof is a sequence of statements such that every statement in the sequence is either

• an instance of an axiom; or
• a deduction from two previous statements using modus ponens.

The latter means that if you have statements $\phi\to\psi$ and $\phi$, you can write down $\psi$. If you think about it, this is really nothing more than expressing the usual interpretation of $\to$ as "if... then".

Here is an example of a formal proof using modus ponens. Strictly speaking, the line numbers and explanations are not part of the proof but they are commonly included in order to assist the reader.

1. $(p\to((p\to p)\to p))\to((p\to(p\to p))\to(p\to p))$ . . . . . axiom 2
2. $\ p\to((p\to p)\to p)$ . . . . . axiom 1
3. $(p\to(p\to p))\to(p\to p)$ . . . . . modus ponens from lines 1,2
4. $\ p\to(p\to p)$ . . . . . axiom 1
5. $\ p\to p$ . . . . . modus ponens from lines 3,4

Thus, we have proved the theorem $p\to p$.

Finding the right sequence of statements efficiently is not always easy and will require practice, although it can be done algorithmically, in effect by starting with the truth table of the required theorem. The algorithm does not usually give the shortest possible proof. You may learn this later in your studies.