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.

-

1
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

3
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

2 Answers

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))$

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)

-

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.

-
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 43, "mathjax_display_tex": 1, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": false, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.9043378829956055, "perplexity_flag": "middle"}