4
$\begingroup$

How could I derive the following proposition:

$$ ((A \rightarrow B) \rightarrow A) \rightarrow A ) $$

using any of the following axioms:

1) $A→(B→A)$

2) $(A→(B→C))→((A→B)→(A→C))$

3) $((¬B)→(¬A))→(A→B)$

  • 2
    You have supplied only axioms, and no rules of inference.2012-02-21
  • 0
    Sorry. Modus ponens should be used.2012-02-21
  • 0
    This is Peirce's law, which is equivalent to (3) in the presence of (1) and (2).2012-02-21
  • 0
    Thanks. I'm still not sure how to prove this. :| I'm pretty new to propositional calculus.2012-02-21
  • 0
    @Arjang: I rolled back your edit since it introduced double arrows that were likely not intended.2012-02-21
  • 0
    @joriki : That that is nice of you to let me know, but that was not double arrow \Rightarrow $\Rightarrow$ it was \implication $\implies$, is it meant to be something other than implication?2012-02-21
  • 3
    @Arjang: It's fairly standard in logic to use $\to$ for the implication symbol in the object language and reserve ⟹ for implication in the metalanguage.2012-02-21
  • 0
    @ChrisEagle : Thank you2012-02-21
  • 0
    @ZhenLin Peirce's law is NOT equivalent to (3) in the presence of (1) and (2). In other words, {A→(B→A), (A→(B→C))→((A→B)→(A→C)), ((¬B)→(¬A))→(A→B)} under detachment is not equivalent to {A→(B→A), (A→(B→C))→((A→B)→(A→C)), ((A→B)→A)→A)} under detachment. {A→(B→A), (A→(B→C))→((A→B)→(A→C)), ((¬B)→(¬A))→(A→B)} under detachment gives you (¬, →) classical propositional calculus, {A→(B→A), (A→(B→C))→((A→B)→(A→C)), ((A→B)→A)→A)} under detachment gives you the implicational propositional calculus.2014-04-28

3 Answers 3