1

I'm trying to construct a formal proof for ((p ⇒ q) ⇒ p) ⇒ p. in Fitch. I know this is true, but how do I prove it?

I can only use And Intro, And Elim, Or Inro, Or Elim, Neg Intro, Neg Elim, Impl Intro, Impl Elim, Biconditional Intro, and Biconditional Elim.

Delgan
  • 18,571
  • 11
  • 90
  • 141
rodrigo ferreira
  • 61
  • 6
  • Related: [How would one prove ((p ⇒ q) ⇒ p) ⇒ p, using the Fitch system](http://stackoverflow.com/questions/42286985/how-would-one-prove-p-%e2%87%92-q-%e2%87%92-p-%e2%87%92-p-using-the-fitch-system) – Delgan Mar 16 '17 at 15:54
  • Can you show what you've tried so far? – EJoshuaS - Stand with Ukraine Mar 16 '17 at 16:06
  • At frist i tried using p => q as assumption [link]http://imgur.com/a/NnSou, but i got into ((p=>q)) => p => p. Now im trying ((p=>q) = > p) as assumption but i have no idea how to get the => p. – rodrigo ferreira Mar 17 '17 at 13:14
  • I just found out that this is Peirce's law. I dont think is possible to reach ((p=>q)) => p => p without a premisse like p=>q. – rodrigo ferreira Mar 17 '17 at 15:01

1 Answers1

0

The following proof uses Klement's Fitch-style proof checker. Description of the symbols and the rules are in forallx. Links to both are below.

enter image description here

A slightly different version is on Philosophy Stack Exchange: https://philosophy.stackexchange.com/a/55395/29944 That would be another place to try to get answers to such questions.

References

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/

Frank Hubeny
  • 178
  • 1
  • 3
  • 10