In Fitch, how does one prove “P” from the premise “(¬P ∨ Q)→P”?

Question

I can't figure out how to prove that formally. Please, help!!

Answer 1

In Fitch, how does one prove “P” from the premise “(¬P ∨ Q)→P”?

One assumes not-P and uses a Reduction To Absurdity proof.

|_ (~P v Q) -> P   Premise
|  |_ ~P           Assumption
|  |  :            :
|  |  :            :
|  |  :            :
|  ~~P             Negation Introduction
|  P               Double Negation Elimination

Answer 2

Here is a way to prove this using the rules in Klement's Fitch-style proof checker. The rules are described in forallx. Both are available in the links below and would make good supplementary material to whatever text you are using.

This proof uses the law of the excluded middle (LEM). To use this I take a simple statement and its negation and from both try to derive the same result. If I get the same result than I can invoke the law of the excluded middle. Here I chose "P" and "¬P", because one of these, "P", is the goal itself.

For "P" I need do nothing but add the subproof with assumption "P". For "¬P" I use disjunction introduction to get line 4 and then conditional elimination on line 5 (modus ponens) to get "P". I reached the goal, "P", in both cases and so I can discharge the two assumptions on line 2 and 3 and reach the end of the proof.

---

Reference

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/