Looking for a simple proof of the independence of the law of excluded middle

Question

I have seen a number of excellent posts on the difference between intuitionist propositional logic (IPL) and classical propositional logic (CPL), all of which state that IPL is agnostic on the law of excluded middle (LEM) or its equivalent forms. I have not seen a clear, simple demonstration that LEM is independent of IPL. Can someone point me in the right direction? It looks like maybe one way to do this involves the BHK interpretation of IPL, with some results about non-computability.

Can someone point me toward a place where that argument is spelled out more? Is there a simple alternative to it? Thanks!

Answer 1

Every Heyting algebra is a model of IPL. Some Heyting algebras (the Boolean algebras) satisfy LEM, and some do not. Therefore, LEM is independent of IPL.

For explicit examples:

• The simplest non-trivial Boolean algebra is $\{0,1\}$ with $0<1$. We have $\lnot 0 = 1$, so $0\vee \lnot 0 = 0 \vee 1 = 1$. Also $1\vee \lnot 1 = 1$. So LEM holds.
• The simplest non-Boolean Heyting algebra is $\{0,\varepsilon,1\}$ with $0<\varepsilon< 1$. We have $\lnot \varepsilon = 0$, so $\varepsilon \vee \lnot \varepsilon = \varepsilon\vee 0 = \varepsilon\neq 1$. So LEM does not hold.

Answer 2

The way we always prove that a certain sentence is independent of some axiom system is to find a model which think the sentence is true, and a model which thinks the sentence is false.

For IPL, there are a few choices of semantics, but I'll be discussing Heyting Algebras. Informally:

Let $(H,\top,\bot,\land,\lor,\Longrightarrow)$ be a Heyting Algebra. Then a valuation $v$ is a function assiging to each primitive proposition $p$ a value $v(p) \in H$. We can extend this valuation to a function (which I'll also call $v$) which takes any sentence in IPL and returns a value in $H$. For instance, $v(p \land q) = v(p) \land v(q)$, where the first $\land$ is logical and, and the second $\land$ is the meet operation in the lattice. Importantly, we interpret $\lnot p$ as an abbreviation for $p \implies \bot$.

We want to think of $\top$, the top element of $H$, as "true", and as $\bot$, the bottom element of $H$, as "false". The other values in $H$ should be thought of as "intermediate" truth values.

Now a theorem:

IPL is Sound and Complete for these semantics

That is, $\text{IPL} \vdash \varphi$ if and only if for every heyting algebra $H$ and for every valuation $v$ taking values in $H$, $v(\varphi) = \top$

Soundness is easy. Just check that the axioms all evaluate to $\top$ in every heyting algebra, and that modus ponens preserves $\top$-ness.

Completeness is also easy, but is a bit trickier conceptually. The idea is that the set of all formulas you can form (with, say, countably many variables) (quotiented out by provable equivalence) is itself a heyting algebra. Then there is a natural valuation map sending $v(p) = p$. Moreover, by definition, $v(\varphi) = \top$ in this algebra exactly when $\text{IPL} \vdash \varphi$.

---

Now, what does this buy us? Well, we want to show first that LEM is not a theorem of IPL. How do we do this? It suffices to find a heyting algebra $H$ so that $v(p \lor \lnot p) \neq \top$. I'll leave it as an instructive exercise in the definition of heyting algebras to find an example. There's a hint below the fold:

Consider finite linear orders

So we know that LEM is not a theorem of IPL. What do we mean when we say that IPL+LEM is classical logic?

Well, if you remember that classical logic is sound and complete for boolean algebras, then to show that IPL+LEM is classical logic, it suffices to show that IPL+LEM is also sound and complete for boolean algebras, because then we have

$$ \text{IPL+LEM} \vdash \varphi \iff v(\varphi) = \top \text{ for every $v$ with values in a boolean algebra} \iff \text{CPL} \vdash \varphi $$

But we know this is true! Since in a boolean algebra we can show $p \lor \lnot p = \top$, we find IPL+LEM is sound in boolean algebras. Conversely, if you run the same argument as before (building a universal model) we can show that it's a boolean algebra, so that IPL+LEM is complete for boolean algebras too.

---

I hope this helps ^_^

Answer 3

The others answers give simple semantic proofs showing that LEM is independent of intuitionistic logic.

However, you don't always need to construct a model to show non-derivability. There are simple, clear proof-theoretic arguments showing the same thing, which have the advantage that they work for intuitionistic first-order predicate logic as well, without any additional work or need for modification.

One of them relies on the following important property satisfied by the intuitionistic calculus.

Disjunction property: For any formulae $M,N$, if there is an intuitionistic derivation of $\vdash M \vee N$, then we can find a derivation of either $\vdash M$ or $\vdash N$.

By the disjunction property, if $\vdash A \vee \neg A$ was provable, then we would be able to prove either $\vdash A$ or $\vdash \neg A$. But it's clear that neither of these have (even classical) derivations. Hence, $\vdash A \vee \neg A$ is not provable.

Okay, that's quick and simple, but how do we prove the disjunction property? Well, intuitionistic logic is usually defined by means of either a sequent calculus deduction system, a natural deduction system, or a Hilbert system. For the sequent calculus, we can prove it simply by looking at cut-free derivations (see [1] for a more general version). For natural deduction, we can either reduce it to the sequent calculus, or prove it directly by proof normalization (see [2]). The Hilbert system is also reducible to the sequent calculus. So I'll give the short sequent calculus version:

Recall that the sequent calculus has the following two rules for introducing $\vee$ on the right of the turnstile $\vdash$:

$$\frac{\Gamma \vdash A}{\Gamma \vdash A \vee B}\vee\!R_1$$

$$\frac{\Gamma \vdash B}{\Gamma \vdash A \vee B}\vee\!R_2$$

If $\vdash M \vee N$ has a derivation, then by the cut-elimination theorem it has a derivation that doesn't use the cut rule. Look at the last rule of a cut-free derivation of $\vdash M \vee N$. It cannot be cut, so it can only be $\vee\!R_1$ or $\vee\!R_2$. If it's $\vee\!R_1$, then the previous line was $\vdash M$, so $\vdash M$ has a derivation as claimed. Otherwise, the last rule is $\vee\!R_2$ and the previous line was $\vdash N$, so $\vdash N$ has a derivation. This proves the disjunction property.

edit: As commenters pointed out, it's worth mentioning that the negation of LEM, $\vdash \neg (A \vee \neg A)$, cannot be derived in intuitionistic logic either. To show this, all you have to do is notice that $\neg (A \vee \neg A) \vdash A$ is provable in intuitionistic logic. So if $\vdash \neg (A \vee \neg A)$ was provable as well, you'd be able to use the cut rule to conclude that $\vdash A $ would also be provable. But as we observed above, during the proof of the disjunction property, $\vdash A$ is not derivable. Thus, $\vdash \neg (A \vee \neg A)$ is not derivable either.

[1] A. S. Troelstra, H. Schwichtenberg: Basic Proof Theory, 2nd edition, 2000. ISBN 9781139168717

[2] D. Prawitz: Natural Deduction: A Proof-Theoretical Study, Dover Publications, 1965. ISBN 9780486446554x