Law of Excluded Middle

Question

I'm here with a question about solving a premiseless proof in a blocks language. With a goal of $\def\Cube{\operatorname {Cube}}\lnot(\Cube(b)\land b=c) \lor \Cube(c)$, is it right to try to prove $(P\lor\lnot P) $first or should I just have tried to do $\lor $-Elim in the first place? It has been difficult to draw contradictions when nothing is established beforehand. Once I get to the form $P \lor\lnot P$, is it possible to prove $\lnot P $?

Answer 1

Simplifying the notation, your proof is :

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

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

3) $P \lor \lnot P$ --- from 2) by $\lor$-introduction

4) $\bot$ --- from 1) and 3) by $\rightarrow$-elimination (or $\bot$-introduction)

5) $\lnot P$ --- from 2) and 4) by $\rightarrow$-introduction, discharging [b]

6) $P \lor \lnot P$ --- from 5) by $\lor$-introduction

7) $\bot$ --- from 1) and 6) by $\rightarrow$-elimination (or $\bot$-introduction)

8) $\lnot \lnot (P \lor \lnot P)$ --- from 1) and 7) $\rightarrow$-introduction, discharging [a]

9) $(P \lor \lnot P)$ --- from 9) by $\lnot$-elimination.

---

Thus, your proof amounts to :

$\vdash P \lor \lnot P$

which is a law of classical logic (we have used $\lnot$-elimination, also called Double Negation, in the proof).

---

---

Having said that, your goal is to prove :

$\lnot(\varphi(b) \land b=c) \lor \varphi(c)$

which is equivalent to :

$(\varphi(b) \land b=c) \rightarrow \varphi(c)$.

This must be so, because it is a simple application of the laws of identity (or equality).

Thus, you have to use the rules for managing "$=$", like [see Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007), page 122 ] :

$$\frac{s = t \quad \varphi[s/x]}{\varphi[t/x]} \quad \text {(=E)}$$

---

Now the proof is straightforward :

1) $\varphi(b) \land b=c$ --- assumed [a]

2) $\varphi(b)$ --- from 1) by $\land$-elimination

3) $b=c$ --- from 1) by $\land$-elimination

4) $\varphi(c)$ --- from 2) and 3) by $=$-elimination

5) $(\varphi(b) \land b=c) \rightarrow \varphi(c)$ --- from 1) and 4) by $\rightarrow$-introduction, discharging [a].