1
$\begingroup$

$$⊢ P ∨ ¬P$$

I found this question on the net. I know the solution, but I find it complicated.

How should I approach this sort of question? Or can you provide me with another solution?

Solution

$\endgroup$
5
  • $\begingroup$ What sort of question? $\endgroup$ – Git Gud Dec 29 '14 at 21:04
  • $\begingroup$ You can find here a slightly different proof. $\endgroup$ – Mauro ALLEGRANZA Dec 30 '14 at 9:18
  • $\begingroup$ As far as I can tell, the accepted answer misses a step (as pointed out by a comment). It only proves $\neg \neg(p \vee \neg p)$. $\endgroup$ – Stefan Perko Dec 30 '14 at 9:43
  • $\begingroup$ What proof system is the given proof derived in? If you found the image online can you provide a source? $\endgroup$ – Calculemus Jan 8 '15 at 4:39
  • 1
    $\begingroup$ @Calculemus danielclemente.com/logica/dn.en-node38.html $\endgroup$ – MUSE Jan 9 '15 at 15:11
0
$\begingroup$

I don't know, whether you really find this helpful, but you could prove a bunch of other (generally useful) statements / rules first:

  • $\neg(p \wedge q) \Rightarrow \neg p \vee \neg q$ (DM)
  • $\neg(p \wedge \neg p)$ (PNC)
  • $(p \vee q, p\vdash p', q \vdash q') \vdash p' \vee q'$ (CDL)

and then it should be easy:

  1. $\neg(p\wedge \neg p)$ (by PNC)

  2. $\neg p \vee \neg \neg p$ (by DM, 1.)

  3. $\neg p \vdash \neg p$ (Assumption rule)

  4. $\neg \neg p \vdash p$ (by $\neg\neg E$)

  5. $p \vee \neg p$ (by CDL, 2.,3.,4.)

Here, for example, the proof for (PNC):

  1. $p \wedge \neg p$ (H)
  2. $\,\,\,\,$ $p$ $\,\,\,\,$ ($\wedge E1, 1.$)
  3. $\,\,\,\,$ $\neg p$ $\,\,\,$ ($\wedge E2, 1.$)
  4. $\,\,\,\,$ $\perp$ $\,\,\,\,$ ($\Rightarrow E$, 2., 3.)
  5. $\neg(p \wedge \neg p)$ ($\Rightarrow I$, 1., 4.)
$\endgroup$
2
  • $\begingroup$ What does PNC and CDL stand for? $\endgroup$ – MUSE Dec 29 '14 at 20:32
  • $\begingroup$ Doesn't really matter, I just gave them names to refer to them. But it stands for "principle of non-contradiction" and "constructive dilemma". (I don't think, this a standard abbreviation) $\endgroup$ – Stefan Perko Dec 29 '14 at 20:40
0
$\begingroup$

$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}$ That is almost correct.   You were aiming at a proof by contradiction, and that needs to use just one subproof (also by contradiction). $$\fitch{}{\fitch{1.~\lnot(p\vee\lnot p)\hspace{10ex}\text{H (assumption or hypothesis)}}{\fitch{2.~p\hspace{15ex}\text{H (assumption)}}{3.~p\vee\lnot p\hspace{10ex}\text{I$\lor$ 2 (disjunction introduction)}\\4.~\lnot(p\lor\lnot p)\hspace{6.5ex}\text{IT1 (reiteration)}}\\5.~\lnot p\hspace{17.5ex}\text{I$\lnot$2,3,4 (negation introduction)}\\6.~p\vee\lnot p\hspace{14ex}\text{I$\lor$ 5 (disjunction introduction)}\\7.~\lnot(p\lor\lnot p)\hspace{10.5ex}\text{IT1 (reiteration)}}\\8.~\lnot\lnot(p\vee\lnot p)\hspace{12.5ex}\text{I$\lnot$ 1,6,7 (negation introduction)}\\9.~p\vee\lnot p\hspace{17.5ex}\text{E$\lnot\lnot$ (double negation elimination, aka DNE)}}$$

Thus the Law of Excluded Middle (LEM) is provable, iff you accept the Double Negation Elimination (DNE) rule of inference.


Note: Some rules systems combine inferences on lines 8 and 9 into one step, and call that the rule of negation elimination (or indirect proof)

$$\fitch{}{\fitch{1.~\lnot(p\vee\lnot p)\hspace{10ex}\text{H (assumption or hypothesis)}}{\fitch{2.~p\hspace{15ex}\text{H (assumption)}}{3.~p\vee\lnot p\hspace{10ex}\text{I$\lor$ 2 (disjunction introduction)}\\4.~\lnot(p\lor\lnot p)\hspace{6.5ex}\text{IT1 (reiteration)}}\\5.~\lnot p\hspace{17.5ex}\text{I$\lnot$2,3,4 (negation introduction)}\\6.~p\vee\lnot p\hspace{14ex}\text{I$\lor$ 5 (disjunction introduction)}\\7.~\lnot(p\lor\lnot p)\hspace{10.5ex}\text{IT1 (reiteration)}}\\8.~p\vee\lnot p\hspace{17.5ex}\text{E$\lnot$ 1,6,7 (negation elimination, aka indirect proof)}}$$

Thus is the Law of Excluded Middle (LEM) provable iff you allow the Indirect Proof (IP) rule of inference... or other equivalent formulations.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.