# Deduction of contraposition propositional logic

I have to find a deduction whose conclusion is the law of contraposition: $(\varphi \rightarrow \psi) \rightarrow (\neg \psi \rightarrow \neg \varphi)$.

In particular it is suggested we use the following axioms:

1. $\varphi \rightarrow (\psi \rightarrow \varphi)$
2. $(\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \neg \psi) \rightarrow \neg \varphi)$

This is as far as I've gotten, but in the end the result is a tautology and not my intended formula:

1. $\varphi \rightarrow \psi \vdash \neg \psi \rightarrow \neg \varphi$ [Deduction theorem]
2. $(\neg \psi \rightarrow \neg \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\neg \psi \rightarrow \neg \varphi))$ [Iteration of 1.]
3. $\varphi \rightarrow \psi$ [Assumption]
4. $(\neg \psi \rightarrow \neg \varphi) \rightarrow (\neg \psi \rightarrow \neg \varphi)$ [Modus ponens of 2 and 3]

How can I get from $(\neg \psi \rightarrow \neg \varphi) \rightarrow (\neg \psi \rightarrow \neg \varphi)$ to $(\neg \psi \rightarrow \neg \varphi)$?

Thank you very much in advance!

• I'm uncomfortable with using the deduction theorem, since it is in itself stronger than the law of contraposition. – Mark Fischler Oct 25 '16 at 21:31
• This was just my idea, I'm sure there is a better and more elegant solution. – Francesco Carzaniga Oct 26 '16 at 7:08

Assume the antecedent of (($\phi$$\rightarrow$$\psi$)$\rightarrow$($\lnot$$\psi$$\rightarrow$$\lnot$$\phi$)).

Then apply 2. and detach something, which I'll call "something".

Now assume the second antecedent of the above '$\lnot$$\psi$'. Then apply axiom 1 and detach something that matches the antecedent of "something".

And I hope you can then find the last step.

Edit:

In Polish notation we have the following as axioms:

1. CaCba
2. CCabCCaNbNa

Here's a diagram:

    CCabCCaNbNa    Cab   C a  C b a
\           /        |    | |
\         /         --   | --
\       / Nb     C Nb C a Nb
\     /   \    /
CCaNbNa  CaNb
\    /
Na

• I'm not sure I understand what you mean. By "assuming the antecedent" I think you mean what I did in the first step with the deduction theorem, and I could also assume $\neg \psi$, as you seem to suggest in your answer, but this doesn't get me anywhere. If you could be a bit more precise also in your usage of "detach" I would be very grateful. – Francesco Carzaniga Oct 26 '16 at 7:11
• Clarification: By following your steps it seems to me you're implying that implication is associative. – Francesco Carzaniga Oct 26 '16 at 7:21
• By "detach" I mean infer using modus ponendo ponens. – Doug Spoonwood Oct 26 '16 at 8:11
• @FrancescoCarzaniga I've added a diagram. – Doug Spoonwood Oct 26 '16 at 8:22
• Thank you very much now it is perfectly clear. – Francesco Carzaniga Oct 26 '16 at 11:05