Proof that a proposition is not provable and that its negation is not provable

Question

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?

Answer 1

$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 : $\nvDash \lnot \lnot \varphi \to \varphi$ and $\nvDash \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].