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?
  • 2
    $\begingroup$ If $A$ is a propositional variable, then neither $A$ nor $\neg A$ are provable in intuitionistic (or for that matter classical) logic. But that's probably not what you're getting at. Could you explain in more detail which kind of "propositions" you want to consider here? Are you speaking about higher-order logic (which seems to be necessary for even formulating the law of excluded middle as a single statement)? $\endgroup$ Commented Nov 5, 2015 at 10:33
  • $\begingroup$ Doesn't this follow from Gödel's incompleteness theorem? Note that "undecidable" means that you can't proove $\phi$ nor $\neg\phi$ (ie decide if $\phi$ is true or false). $\endgroup$
    – skyking
    Commented Nov 5, 2015 at 10:48

1 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].

  • $\begingroup$ Do you have the proof of the first assumption (in IL) $\endgroup$
    – larsr
    Commented Nov 5, 2015 at 10:40
  • 1
    $\begingroup$ @larsr: If you have a semantics for IL available (e.g. Kripke models), it is easy to exhibit a model in which $A\lor\neg A$ evaluates as false at one node. This cannot happen for a provable formula. $\endgroup$ Commented Nov 5, 2015 at 10:45
  • $\begingroup$ Can it be proved inside the logic itself (i.e. about itself)? Concretely, could I write a Coq proof of it? If the answer is yes, I think one could write a proof showing that adding LEM is actually not irrefutable, and thereby contradicting the proof I linked to... $\endgroup$
    – larsr
    Commented Nov 5, 2015 at 11:10
  • $\begingroup$ @larsr: how do you propose to state "$A \lor \lnot A$ is not provable" as a sentence of the logic itself? In other words, which specific sentence are you asking to be proved in the logic? $\endgroup$ Commented Nov 5, 2015 at 11:40
  • $\begingroup$ I ask because the standard way to show something is unprovable is to use the metatheory (e.g. by using a completeness or soundness theorem). Can you give any example of an analogous result in first-order logic that compares to the one you want here for intuitionistic logic? $\endgroup$ Commented Nov 5, 2015 at 11:50

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .