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!

  • 1
    $\begingroup$ I'm uncomfortable with using the deduction theorem, since it is in itself stronger than the law of contraposition. $\endgroup$ – Mark Fischler Oct 25 '16 at 21:31
  • $\begingroup$ This was just my idea, I'm sure there is a better and more elegant solution. $\endgroup$ – 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.


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
              \    /
  • $\begingroup$ 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. $\endgroup$ – Francesco Carzaniga Oct 26 '16 at 7:11
  • $\begingroup$ Clarification: By following your steps it seems to me you're implying that implication is associative. $\endgroup$ – Francesco Carzaniga Oct 26 '16 at 7:21
  • $\begingroup$ By "detach" I mean infer using modus ponendo ponens. $\endgroup$ – Doug Spoonwood Oct 26 '16 at 8:11
  • $\begingroup$ @FrancescoCarzaniga I've added a diagram. $\endgroup$ – Doug Spoonwood Oct 26 '16 at 8:22
  • $\begingroup$ Thank you very much now it is perfectly clear. $\endgroup$ – Francesco Carzaniga Oct 26 '16 at 11:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.