Prove for the calculus of propositions: $$ A\rightarrow B\mapsto(B\rightarrow C)\rightarrow(A\rightarrow C) $$ I had used axioms and most suitable was this one: $$ X\rightarrow Y\rightarrow(X\rightarrow(Y\rightarrow Z)\rightarrow(X\rightarrow Z)) $$ (axiom2). Then I used Modus ponens rule and got this result: $$ A\rightarrow B,\ A\rightarrow B\rightarrow (A\rightarrow(B\rightarrow C)\rightarrow(A\rightarrow C))\\ A\rightarrow(B\rightarrow C)\rightarrow(A\rightarrow C) $$

Then I didn't understand, how to get $(B\rightarrow C)\rightarrow(A\rightarrow C)$. What axiom should I use or rule?


Using the Deduction Theorem:

  1. $A \to B$ --- premise

  2. $B \to C$ --- assumed [a]

  3. $(B \to C) \to (A \to (B \to C))$ --- Ax.1

  4. $A \to (B \to C)$ --- from 2) and 3) by Modus Ponens

  5. $(A \to B) \to ((A \to (B \to C)) \to (A \to C))$ --- Ax.2

  6. $((A \to (B \to C)) \to (A \to C))$ --- from 1) and 5) by Modus Ponens

  7. $A \to C$ --- from 4) and 6) by Modus Ponens.

  1. $(B \to C) \to (A \to C)$ --- from 2) and 7) by DT, discharging assumption [a]
  • $\begingroup$ i have a question: could we use Deduction Theorem for this one:$A→B,B→C↦A→C$? $\endgroup$
    – sjr_25
    Jun 17 at 18:44
  • $\begingroup$ @sjr_25 - YES. Modify the above proof assuming also $A$, followed by MP twice to get $C$ and then conclude by DT with $A \to C$. $\endgroup$ Jun 18 at 5:50
  • $\begingroup$ Can I ask another question on this topic? $\endgroup$
    – sjr_25
    Jun 18 at 6:26
  • $\begingroup$ @sjr_25 - why not ? $\endgroup$ Jun 18 at 6:43
  • $\begingroup$ Can i rewrite this ¬ A,¬ B→(¬ AVB)→(AV¬B) like A⟷B $\endgroup$
    – sjr_25
    Jun 18 at 6:58

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.