Proof that a proposition is not provable and that its negation is not provable Many propostions are not provable within (some) logic, i.e. LEM, the law of the excluded middle is not provable within IL, intutionistic logic. (However, LEM is not inconsistent with IL, see here for a proof ). My question is the following: _Is there an example of_ * _a proposition that is provably unprovable in IL, and_ * _whose negation is **also** provably unprovable in IL?_

$A \lor \lnot A$ is not provable in IL.

See : Dirk van Dalen, Logic and Structure (5th ed - 2013), **Ch.6.3 Kripke Semantics** , page 164-on, and page 166 for a model showing : $\
vDash \lnot \lnot \varphi \to \varphi$ and $\
vDash \varphi \lor \lnot \varphi$.

$\lnot \lnot (A \lor \lnot A)$ is provable in IL.

Thus, by consistency :

> $\lnot (A \lor \lnot A)$

is **not** provable in IL.

* * *

Here is the proof in IL of $\lnot \lnot (A \lor \lnot A)$ :

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

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

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

4) $\bot$ --- from 1) and 3)

5) $\lnot A$ --- from 2) and 4) by $\lnot$-intro, discharging [b]

6) $A \lor \lnot A$ --- from 5) by $\lor$-intro

7) $\bot$ --- from 1) and 6)

> 8) $\lnot \lnot (A \lor \lnot A)$ --- from 1) and 7) by $\lnot$-intro, discharging [a].