Construct a proof for the argument: P ∨ Q, ¬Q ∴ P

Question

Could you please help me to complete my proof using (only) : ∧I, ⊃I, ∨I, ≡I, ∧E, ⊃E, ∨E, ≡E, ¬I and ¬E.

P ∨ Q, ¬Q ∴ P

I tried this proof, on http://proofs.openlogicproject.org/ : but it seems that is not ok.

Answer 1

Your proof is almost there. $$\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{~~1.~P\vee Q\\~~2.~\neg Q}{~~3.~P\vee Q\hspace{10ex}\mathsf R~1\\\fitch {~~4.~P}{}\\\fitch{~~5.~Q}{\fitch{~~6.~\neg P}{~~7.~Q\hspace{10ex}\mathsf R~5\\~~8.~\neg Q\hspace{8.5ex}\mathsf R~2\\~~9.~\bot\hspace{10ex}\neg\mathsf E~7,8}\\10.~\neg\neg P\hspace{9ex}\neg \mathsf I~6{-}9\\11.~P\hspace{12ex}\neg\neg\mathsf E~10}\\12.~P\hspace{13ex}\vee\mathsf E~1,4{-}4,5{-}10}$$

Notes:

• You do not need to reiterate the first premise.  It is not wrong, and does put the disjunction immediately before the two subproofs so makes the proof by cases clear; however, that placement is not required.

• Reiterating $Q$ and $\neg Q$ is likewise technically unnecessary.  It is not wrong, but some proof checkers will insist on it.

• You did not have a double negation elimination rule ($\neg\neg\mathsf E$) listed, and from the way you were attempting $\neg\mathsf I$ it is possible that your proof system implements negation introduction and elimination rules differently to the proof checker's variant.  You may have been going for what the checker calls Indirect Proof ($\mathsf{IP}$) which combines step 10 and 11 into one inference. (Also known as RAA, Reductio Ad Absurdum.)

• Indeed, that little subproof is more common in systems which do not implement a falsum symbol ($\bot$) to indicate an absurdity.   Systems which include $\bot$, typically use a rule of explosion (or Ex Falso Quodlibet, EFQ) for this; see rule $X$ in the checker.

You may have expected the proof to look like this.$$\fitch{~~1.~P\vee Q\\~~2.~\neg Q}{~~3.~P\vee Q\hspace{10ex}\mathsf R~1\\\fitch {~~4.~P}{}\\\fitch{~~5.~Q}{\fitch{~~6.~\neg P}{~~7.~Q\hspace{10ex}\mathsf R~5\\~~8.~\neg Q\hspace{8.5ex}\mathsf R~2}\\~~9.~P\hspace{11ex}\neg \mathsf I~6{-}8\quad(\mathrm{IP})}\\10.~P\hspace{13ex}\vee\mathsf E~1,4{-}4,5{-}9}$$Okay, that will not work on this proof checker, but might be valid in your own proof system.

Answer 2

Hint:

The idea is correct, we do need $\lor$ Elim on $P\lor Q$, but the general structures of the proof would be

Before read the answer, see if you can fill the blank.

Answer:

Update:

Here I'll just add another proof without $\bot$ Elim and $\bot$ Intro, but require double negation rule.

I'm not sure it can be proved only by the rules you listed, $\equiv$ Elim and $\equiv$ Intro are not even defined in the editer.