2

FYI, the logic program I use cannot do contradiction introductions. This point is most likely irrelevant, for I highly doubt I would need to use any form of contradiction for this proof.

In my attempt to solve this, I started off with assuming (p ⇒ q) ⇒ p)
Is this correct?

If so, what next? Forgive me if the solution seems so obvious.

God's Drunkest Driver
  • 135
  • 9
  • The proof I provided for another question uses contradiction introduction so it may not be acceptable: https://stackoverflow.com/a/53454649/6055422 There are proofs in Wikipedia under Peirce's rule: https://en.wikipedia.org/wiki/Peirce%27s_law But they may not work either given the restriction on the rules you may use. – Frank Hubeny Nov 24 '18 at 02:32

1 Answers1

0
(p ⇒ q) ⇒ p
((p ⇒ q) ⇒ p) ∨ (p ⇒ p)        ; (X ⇒ X) and Or introduction
((p ⇒ q) ∨ p) ⇒ p              ; (X ⇒ Z) ∨ (Y ⇒ Z) |- (X ∨ Y ⇒ Z)
((¬p ∨ q) ∨ p) ⇒ p             ; (p ⇒ q) ⇔ (¬p ∨ q)
((¬p ∨ p) ∨ q) ⇒ p             ; (X ∨ Y) ∨ Z |- (X ∨ Z) ∨ Y
(true ∨ q) ⇒ p                 ; (¬X ∨ X) ⇔ true
true ⇒ p                       ; (true ∨ X) ⇔ true
p                              ; Implication elimination
((p ⇒ q) ⇒ p) ⇒ p              ; Implication introduction
Leandro Caniglia
  • 14,495
  • 4
  • 29
  • 51
  • many of the steps in this solution cannot be simply arrived at using the 10 rules of inference, namely, And Intro, And Elim, Or Inro, Or Elim, Neg Intro, Neg Elim, Impl Intro, Impl Elim, Biconditional Intro, and Biconditional Elim. I cannot use propositional resolution: (p ⇒ q) ⇔ (¬p ∨ q). I would have to prove (p ⇒ q) ⇔ (¬p ∨ q) using those 10 rules I mentioned, within the proof of (p ⇒ q) ⇒ p – God's Drunkest Driver Feb 24 '17 at 18:12
  • @AndrewGuo what's your definition of `p ⇒ q`? – Leandro Caniglia Feb 24 '17 at 19:30
  • p implies q (my comment has to be 15 characters in length so I will add this parenthetical) – God's Drunkest Driver Feb 24 '17 at 20:09
  • @AndrewGuo a sentence, namely 'p implies q' is not a definition. The commonly accepted definition of `p ⇒ q` is precisely `¬p ∨ q`, which I used in my answer. If you want a proof of `(p ⇒ q) ⇔ (¬p ∨ q)` you have to provide a definition of `(p ⇒ q)`. – Leandro Caniglia Feb 24 '17 at 20:46