4
$\begingroup$

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.

  • 0
    @QiaochuYuan So, sure this question and your comment comes as old, but there do exist systems of logic where you have the rule referenced by the author, but don't have the rule "From $\gamma$, $\alpha$ $\vdash$ $\beta$, you may infer $\gamma$, $\vdash$ C$\alpha$$\beta$." In my opinion, to best understand how the deduction theorem works, you need to write a deduction with assumptions, and then convert that deduction into a "pure" axiomatic proof using the algorithmic procedure that a meta-proof of the deduction theorem gives you.2013-08-17

1 Answers 1

9

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.