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

Question

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.

Answer 1

This is small enough for a truth table.

1. First, write out the unmodified table for reference:

   P1 P2 P1->P2
   0 0 1
   0 1 0
   1 0 1
   1 1 1

2. Next, apply the negation from the antecedent:

   ~P1 P2 ~P1->P2
   1 0 1
   1 1 1
   0 0 1
   0 1 0

3. Then, apply the negation from the consequent:

   ~P2 P1 ~P2->P1
   1 0 1
   0 0 1
   1 1 1
   0 1 0

Both of the modified truth tables match, so they are logically equivalent.

Answer 2

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.