Law of Excluded Middle 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 $?

 A: 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].

