Give a natural deduction proof of the formula "$p ∨ (p → q)$"

Question

I am currently studying Fitch-style natural deduction and I am having trouble proving $p ∨ (p → q)$ without being given a premise.

Below is something I've tried. But it doesn't seem right at all. I'm only using basic intro/elim rules with LEM.

Help is greatly appreciated :)

Answer 1

Hint

Since you have LEM, if you can show $p\vdash p\lor (p\to q)$ and $\lnot p\vdash p\lor(p\to q)$ then you can get the result by $\lor$-elimination on $p\lor \lnot p.$ The first is obvious. The second isn't too bad either (clearly you need to take the right branch).

Answer 2

$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline #2\end{array}}$

I'm only using basic intro/elim rules with LEM.

You will also need the principle of explosion (ex falso quodlibet).

The shape of a LEM proof is a proof by cases, with the cases being a positive and its negation.

$\fitch{}{\fitch{p}{\vdots\\p\vee(p\to q)}\\\fitch{\neg p}{\fitch{\ldots}{\vdots}\\\vdots\\p\vee (p\to q)}\\p\vee(p\to q)}$

---

If you have double negation elimination , you can use a Proof by Contradiction. Assume $\neg(p\vee(p\to q))$ and derive a contradiction, introducing a negation and eliminating the double negation.

Hint: further assuming $p$ will be of use.

$$\fitch{}{\fitch{\neg(p\vee(p\to q))}{\fitch{p}{~\vdots}\\~\vdots\\\bot}\\\neg\neg(p\vee (p\to q))\\p\vee(p\to q)}$$

Answer 3

I'm not sure if I did this right

$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \fitch{}{\fitch{~~1.~~p}{~~2.~~p\vee(p\to q)\hspace{5ex}{\vee}\mathrm I~1}\\\fitch{~~3.~~\neg p}{\fitch{~~4.~~p}{~~5.~~\mathcal F\hspace{11ex}\neg\mathrm E~3,4\\~~6.~~\neg\neg q\hspace{9ex}\neg\mathrm I~5\\~~7.~~q\hspace{12ex}\neg\mathrm E~6}\\~~8.~~p\to q\hspace{11ex}{\to}\mathrm I~4{-}7\\~~9.~~p\vee (p\to q)\hspace{5ex}{\vee}\mathrm I~8}\\10.~~p\vee(p\to q)\hspace{8.5ex}{\vee}\mathrm E~\text{LEM}, 1{-}2, 3{-}9}$

Answer 4

Rather than writing the proof out and hoping it is correct, you can test the proof using a Fitch-style proof checker. Here is how this proof checker would prove the result without using premises:

To use this proof checker for this problem enter "Pv(P>Q)" in the "Conclusion:" box and click "Create Problem". This will set up your problem and you can enter the lines as above.

I use the law of the excluded middle in this proof. To use that I have to consider both sides of the disjunction $P \lor \neg P$. I will consider each side in a separate subproof. That is, I will assume one side of the disjunction in each subproof and then derive the desired result.

The first side I considered on lines 1 to 2. I derived the desired result $P \lor (P \to Q)$ almost immediately by using conjunction introduction ($\lor$I).

The second side I considered on lines 3 to 8. Note how on line 4 I assumed $P$ in order to derive a contradiction with the assumption on line 3. With a contradiction I can derive anything so I derive $Q$ on line 6 because that is what I will need to derive the implication on line 7.

When both sides reached the desired conclusion I could reference the law of the excluded middle to close both subproofs and derive the desired result.

The proof checker and online textbook giving more information can be accessed through the links below.

---

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, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf