4
$\begingroup$

I'm taking a course from Stanford in Logic. I'm stuck with an exercise where I'm doing some proof. The Fitch system I'm given only allows

  • $ \land $ introduction and elimination
  • $ \lor $ introduction and elimination
  • $ \to $ introduction and elimination
  • $ \equiv $ introduction and elimination
  • $ \lnot$ introduction and
  • $ \lnot \lnot $ elimination

but not

  • $ \bot $ introduction and elimination

I've been struggling to prove the law of excluded middle (``p ∨ ¬p`) within this system. All of the proofs I've seen online make use of $\bot$ elimination to prove it by contradiction:

| ~(p | ~p)  (assumption)
| | p        (assumption)
| | p | ~p   (or introduction)
| | $\bot$
|
| | ~p       (assumption)
| | p | ~p   (or introduction)
| | $\bot$
|
| (p | ~p)   (proof by contradiction)

Since I can't use $\bot$ elimination, I was trying to do this with $ \lnot$ introduction:

| ~(p | ~p)  (assumption)
| | ???
| ~(p | ~p) => x
|
| | ???
| ~(p | ~p) => ~x
| p | ~p     (not introduction)

but I just can't get it. I can't figure out how to get x and ~x.

Is this provable without $\bot$ elimination? If so, what are the steps?


Background:

What I'm ultimately trying to prove is this: Given p ⇒ q, use the Fitch System to prove ¬p ∨ q. I'm able to prove that p ⇒ ¬p ∨ q and that ¬p ⇒ ¬p ∨ q, but I need to be able to plug p ∨ ¬p into the proof to be able to do 'or elimination'.

$\endgroup$
  • 1
    $\begingroup$ @GitGud I fixed it to not go through Coursera, but directly to the Stanford website. $\endgroup$ – Tudor Timi Dec 11 '16 at 19:21
  • $\begingroup$ You have to use double negation elim. $\endgroup$ – Mauro ALLEGRANZA Dec 11 '16 at 19:25
  • $\begingroup$ I'm confused. What's wrong with the proof that appears after clicking show answer? $\endgroup$ – Git Gud Dec 11 '16 at 19:25
  • 1
    $\begingroup$ The basic idea is to prove $\lnot \lnot (P \lor \lnot P)$, then use double elim. In constructive logic $\lnot \lnot X$ basically means $X$ is consistent, instead of $X$ is true, so those type of theorems are much easier to establish. $\endgroup$ – DanielV Dec 11 '16 at 19:54
  • 1
    $\begingroup$ @TudorTimi I conjectured so. Well, that settles it, then. $\endgroup$ – Git Gud Dec 11 '16 at 21:57
6
$\begingroup$

1) $\lnot (A \lor \lnot A)$ --- assumed [a]

2) $A$ --- assumed [b]

3) $A \lor \lnot A$ --- from 1) by $\lor$-intro

4) $\lnot A$ --- from the contradiction : 2) and 3) by $\lnot$-intro, discharging [b]

5) $A \lor \lnot A$ --- $\lor$-intro

6) $\lnot \lnot (A \lor \lnot A)$ --- from the contradiction : 1) and 5) by $\lnot$-intro, discharging [a]

7) $A \lor \lnot A$ --- from 6) by $\lnot \lnot$-elim.


For the different "flavours" of the negation rules in Natural Deduction you can see :


Your idea regarding the proof : $P \to Q \vdash \lnot P \lor Q$ is correct: you can use the "derived" rule :

$$\dfrac { } {\lnot P \lor P}$$

Alternatively :

0) $A \to B$ --- premise

1) $\lnot A$ --- assumed [a]

2) $\lnot A \lor B$ --- by $\lor$-intro

3) $\lnot (\lnot A \lor B)$ --- assumed [b]

4) $\lnot \lnot A$ --- from 1) with contradiction : 2) and 3) by $\lnot$-intro, discharging [a]

5) $A$ --- from 4) by $\lnot \lnot$-elim

6) $B$ --- from 0) and 5) by $\to$-elim

7) $\lnot A \lor B$ --- $\lor$-intro

8) $\lnot \lnot (\lnot A \lor B)$ --- from 3) with contradiction : 7) and 3) by $\lnot$-intro, discharging [b]

9) $\lnot A \lor B$ --- from 8) by $\lnot \lnot$-elim

Thus, from 0) and 9) :

$A \to B \vdash \lnot A \lor B$.

$\endgroup$
  • $\begingroup$ The Fitch system in my course does not introduction differently than how you did it. A→B, A→¬B ⊢ ¬A. $\endgroup$ – Tudor Timi Dec 11 '16 at 22:12
  • $\begingroup$ @TudorTimi - perfect. $\endgroup$ – Mauro ALLEGRANZA Dec 12 '16 at 6:46
2
$\begingroup$

After @GitGud's comment about the answer to my initial question being available here after clicking Show answer, I had a look at the proof and I got inspired on how to do this for p | ~p:

 0.                               (no premises)
 1. *    ~(p | ~p)                (assumption)
 2. **     p                      (assumption)
 3. **     p | ~p                 (or introduction 2.)
 4. *    p => p | ~p              (implication introduction 2., 3.)
 5. **     p                      (assumption)
 6. **     ~(p | ~p)              (reiteration 1.)
 7. *    p => ~(p | ~p)           (implication introduction 5., 6.)
 8. *    ~p                       (negation introduction 4., 7.)
 9.    ~(p | ~p) => ~p            (implication introduction 1., 8.)
10. *    ~(p | ~p)                (assumption)
11. **     ~p                     (assumption)
12. **     p | ~p                 (or introduction 11.)
13. *    ~p => p | ~p             (implication introduction 11., 12.)
14. **     ~p                     (assumption)
15. **     ~(p | ~p)              (reiteration 10.)
16. *    ~p => ~(p | ~p)          (implication introduction 14., 15.)
17. *    ~~p                      (negation introduction 13., 16.)
18.    ~(p | ~p) => ~~p           (implication introduction 10., 17.)
19.    ~~(p | ~p)                 (negation introduction 9., 18.)
20.    p | ~p                     (negation elimination 19.)
$\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.