# Metalogic: Prove $\{\neg P_1 \to P_2\} \vdash (\neg P_2\to P_1)$ without using the Deduction Theorem

I want to prove that $$\{\neg P_1\to P_2\} \vdash (\neg P_2\to P_1)$$ without using the Deduction Theorem.

I'm not sure how to proceed. The class notes are all we have to work from, no text to work on similar proofs.

-
What axioms and deduction rules are you working from? –  Qiaochu Yuan Apr 28 '11 at 0:47
only modus ponems –  Daniel Lopez Apr 28 '11 at 1:26
and my 3 axiom schemas which are 1. B->(A->B) 2. (~A->B)->((~A->~B)->A) 3. (A->(B->C))->((A->B)->(A->C)) –  Daniel Lopez Apr 28 '11 at 1:27
Please try to put the question in the body of your message; would you require a reader of a book to look up important information on the spine? –  Arturo Magidin Apr 28 '11 at 2:14
I was asked a similar question once, and I responded by going through the proof of the deduction theorem and writing down the steps it gives for this particular case. This is a good exercise in understanding how the deduction theorem works, and technically you have not cited the deduction theorem to do it. –  Qiaochu Yuan Apr 28 '11 at 3:27

I will use the axioms you wrote on the comment, namely:

1. $B\to(A\to B)$
2. $(\lnot A\to B)\to((\lnot A\to\lnot B)\to A)$
3. $(A\to(B\to C))\to((A\to B)\to(A\to C))$

Please add them in your original question to make it complete.

We want to prove $\{\lnot P_1\to P_2\}\vdash\lnot P_2\to P_1$. A proof is a finite sequence of sentences that each of them is either an assumption, or one of the logical axioms or it's a sentence that can be deduced through modus ponens using previous sentences of the proof. I will write a number next to every sentence to denote the step in which I am.

The first thing to do is to write down your assumptions:

1.$\lnot P_1\to P_2$ (assumption)

What we want to do now is to find an axiom that looks like the assumption so we can use the modus ponens. Axiom 2 fits perfectly here so our second step can be

2.$(\lnot P_1\to P_2)\to((\lnot P_1\to\lnot P_2)\to P_1)$ (axiom 2)

Using modus ponens on 1 and 2 we can derive the following

3.$(\lnot P_1\to\lnot P_2)\to P_1$ (modus ponens 1,2)

The "right hand side" of the consequence we want to prove is there (namely $P_1$) but the "left hand side" is different. So what we want is some means to replace that $\lnot P_1\to\lnot P_2$ with $\lnot P_2$. Intuitively, what we need is to show that from $\lnot P_2$ we can derive $\lnot P_1\to\lnot P_2$. Looking at the axioms this is exactly what the first one gives:

4.$\lnot P_2\to(\lnot P_1\to\lnot P_2)$ (axiom 1)

We have something of the form $A\to B$ and $B\to C$ and we want to prove $A\to C$. If we can do that then our prove will be complete.

So now what we want to prove is $\{A\to B, B\to C\}\vdash A\to C$.

Again let's begin with our assumptions:

1.$A\to B$ (assumption)

2.$B\to C$ (assumption)

What we want to do is to create somewhere $A\to C$. Looking at the axioms that you have (and since $A\to B$ is an assumption) a good idea is to use the third axiom

3.$(A\to (B\to C))\to((A\to B)\to(A\to C))$ (axiom 3)

Since $B\to C$ is an assumption we should use the first axiom to create that $(A\to (B\to C))$ we have

4.$(B\to C)\to(A\to (B\to C))$ (axiom 1)

Now we have everything we want. We just need to apply modus ponens to derive our result:

5.$A\to(B\to C)$ (modus ponens 2,4)

6.$(A\to B)\to(A\to C)$ (modus ponens 3,5)

7.$A\to C$ (modus ponens 1,6)

So writing it down a bit more formally we have:

A. $\{A\to B, B\to C\}\vdash A\to C$:

1. $A\to B$ (assumption)
2. $B\to C$ (assumption)
3. $(A\to (B\to C))\to((A\to B)\to(A\to C))$ (axiom 3)
4. $(B\to C)\to(A\to (B\to C))$ (axiom 1)
5. $A\to(B\to C)$ (modus ponens 2,4)
6. $(A\to B)\to(A\to C)$ (modus ponens 3,5)
7. $A\to C$ (modus ponens 1,6)

B. $\{\lnot P_1\to P_2\}\vdash\lnot P_2\to P_1$:

1. $\lnot P_1\to P_2$ (assumption)
2. $(\lnot P_1\to P_2)\to((\lnot P_1\to\lnot P_2)\to P_1)$ (axiom 2)
3. $(\lnot P_1\to\lnot P_2)\to P_1$ (modus ponens 1,2)
4. $\lnot P_2\to(\lnot P_1\to\lnot P_2)$ (axiom 1)
5. $\lnot P_2\to P_1$ (using A with 3,4)

I hope that was helpful.

-