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.
 A: I will use the axioms you wrote on the comment, namely: 


*

*$B\to(A\to B)$

*$(\lnot A\to B)\to((\lnot A\to\lnot B)\to A)$

*$(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$:


*

*$A\to B$ (assumption)

*$B\to C$ (assumption)

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

*$(B\to C)\to(A\to (B\to C))$ (axiom 1)

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

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

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


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


*

*$\lnot P_1\to P_2$ (assumption)

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

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

*$\lnot P_2\to(\lnot P_1\to\lnot P_2)$ (axiom 1)

*$\lnot P_2\to P_1$ (using A with 3,4)


I hope that was helpful.
