Show the following propositions through natural deduction and the Law of Excluded Middle

Question

I have 2 propositions and I don't understand the solution.

$\vdash (p \Rightarrow q) \lor (q \Rightarrow r) $

(LTE = LEM)

I don't understand lines 9 and 10. What is that supposed to mean? If I assume $\lnot q$ then $(q \Rightarrow r)$ is always true, making the proposition true? I don't understand what that symbol on line 9 is supposed to do (I know it means the formula is a contradiction but I don't understand how it's being used here).

$\lnot (\lnot p \lor q) \vdash p$

The Law of the excluded middle is not required for this one.

Same as above. Does it mean that if I assume $\lnot p = 1$ then that makes $(\lnot p \lor q)$ true which makes the left hand side a contradiction? If yes how does that help me?

I have one last question: if I am not told to use the LEM, how do I know when to use it?

Answer 1

For your first question, I think they are using the Principle of Explosion, which says that from a contradiction, anything is provable. An argument for this might go as follows: assume that $p\wedge \neg p$ holds for some proposition $p$ and take any proposition $q$. Then, $p\rightarrow q$ is a true statement because $\neg p$ is true (by assumption). Then, since $p$ is also true, Modus Ponens implies that $q$ holds as well.

For the second question, it seems like $\bot$ is being used to end a proof by contradiction. Namely, if we want to prove that $\neg q$ is true by contradiction, we assume that $q$ is true and deduce $\bot$. This allows us to conclude $\neg q$ by "introducing $\neg$". In the situation you provided, since we want to prove $\neg\neg p$, we assume $\neg p$ and deduce $\bot$. Then we use that $\neg\neg p\rightarrow p$ to conclude that $p$ holds.

There isn't a good rule that necessarily implies that you will be using the Law of Excluded Middle. However, one reason I might think about using it in the first case but not the second is that, in your first example, we have to prove something without using any additional assumptions. In circumstances like this, using LEM would allow us to do a proof by cases where we are allowed to assume something that might help us. In your second example, though, you're proving an implication $A\rightarrow B$ and so in the first line of our proof we get to assume that $A$ is true.

Answer 2

The first proof uses the Principle of Explosion, which states that from a contradiction, anything follows. An alternative way to write this part of the proof would be like this:

$(8)$ Assume $q$
$(9)$ Assume $\lnot r$
$(10)$ Contradiction between $(7)$ and $(8)$
$(11)$ Close assumption at $(9)$: contradiction implies $r$ (proof by contradiction)
$(12)$ Close assumption at $(8)$: $q$ yields $r$ so $q \to r$ (introduction of implication)

This is equivalent to the proof you have, but it requires some extra lines and nested assumptions so for the sake of simplicity this is often instead motivated by the Principle of Explosion.

For your second proof, you are correct that because we've assumed $\lnot p,$ we can infer $\lnot p \vee q$ because $\lnot p$ is taken to be true, so the value of $q$ is unimportant. This is the rule of addition, or introduction of disjunction as it would be called in natural deduction. This helps because now we get a direct contradiction with our premise, which allows us to conclude $p$ by a proof by contradiction. (or reductio ad absurdum if you're into Latin) Essentially if $p$ was false we must have a contradiction, so $p$ must be true.

And as far as when to use $LEM$ or not use $LEM,$ I'd say use it when you can use it and it's useful.

Hope this helps!

Answer 3

don't understand lines 9 and 10. What is that supposed to mean?

Line 9 is by 'negation elimination'. From $~q~$ and $~\lnot q~$ you may infer $~\bot~$. The symbol is the contradiction constant, also known as 'falsum' or 'bottom'. (From any statement and its own negation you may infer that you have a contradiction). Some systems call this 'contradiction introduction'.$$\dfrac{q\quad\lnot q}{\bot}{\lnot_\mathsf e}$$

Line 10 is by 'contradiction elimination', also known as 'ex falso quadlibet' or the 'principle of explosion' (or just 'explosion'). "Anything may be derived from a contradiction". So from $\bot$ we may conclude anything, such as $r$.$$\dfrac{\bot}{r}{\bot_\mathsf e}$$

---

For the second, line 5 is 'negation introduction'. When you derive a contradiction under an assumed position, you may discharge that assumption to deduce the negation of that position.   The distinction between this rule and the last is in the discharging of the assumption. $$\dfrac{\dfrac{[\varphi]^\mathrm n\\~~~\vdots}{\bot}}{\lnot \varphi}{{\lnot_\mathsf i}^\mathrm n}$$

---

Every LEM proof can be rewritten into a double negation elimination proof, and vice versa.
In this case, you can do $$\def\fitch#1#2{~~~~\begin{array}{|l}#1\\\hline #2\end{array}}\fitch{\lnot(\lnot p\vee q)}{\fitch{\lnot p}{\lnot p\vee q\qquad\vee_\mathsf i\\\bot\qquad\lnot_\mathsf e}\\\lnot\lnot p\qquad\lnot_\mathsf i\\p\qquad\lnot\lnot_\mathsf e}\qquad\fitch{\lnot(\lnot p\vee q)}{p\vee\lnot p\qquad\textsf{LEM}\\\fitch{p}{}\\\fitch{\lnot p}{\lnot p\vee q\qquad\vee_\mathsf{i}\\\bot\qquad\lnot_\mathsf e\\p\qquad\bot_\mathsf e}\\p\qquad\vee_\mathsf e}$$

The decision as to which to use is often a choice of style. Here the DNE proof looks more elegant.

---

Usually though there is not that much difference in complexity. Here's the framework for your first proof, as both DNE and LEM style.

$$\fitch{}{\fitch{\lnot((p\to q)\lor(q\to r))}{\fitch{q}{\fitch{p}{q}\\p\to q\\(p\to q)\lor(q\to r)\\\bot\\r}\\q\to r\\(p\to q)\lor(q\to r)\\\bot}\\\lnot\lnot((p\to q)\lor(q\to r))\\(p\to q)\lor(q\to r)}\quad\fitch{}{q\lor\lnot q\\\fitch{q}{\fitch{p}{q}\\p\to q\\(p\to q)\lor(q\to r)}\\\fitch{\lnot q}{\fitch{q}{\bot\\r}\\q\to r\\(p\to q)\lor(q\to r)}\\(p\to q)\lor(q\to r)}$$

Answer 4

Others, particularly Graham Kemp, have given you excellent answers to your specific questions. But standing back a bit from the details, I suspect that you probably need to be doing more background homework about this kind of natural deduction system -- in particular, one deploying the absurdity constant. (As a general principle, if one textbook is leaving you puzzled, do try another!)

The excellent forallX text is brisk but good on ND and is freely available https://forallx.openlogicproject.org/forallxyyc.pdf -- look at Chapters 15 to 18.

Or, for more detail and lots of worked answers to exercises available online, your can also freely download my Intro to Formal Logic from https://www.logicmatters.net/ifl and look at the ND chapters in that.