7
$\begingroup$

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!

$\endgroup$

3 Answers 3

11
$\begingroup$

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.
$\endgroup$
1
  • 2
    $\begingroup$ The three answers I've received are all great. Wish I could accept all of them! But since I asked for a simple proof, I think I have to accept this one! Thank you. $\endgroup$
    – Nat Kuhn
    Nov 25, 2021 at 2:53
11
$\begingroup$

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

$\endgroup$
11
  • $\begingroup$ (+1) Really nice, and conceptually clear! Plus it gets at the (implied) question about LEM and "noncomputability", which the semantic answers don't address $\endgroup$ Nov 23, 2021 at 19:43
  • 2
    $\begingroup$ Maybe for part of the answer, it might be useful to mention the Goedel translation which is used to show that if intuitionistic first-order logic is consistent, then classical first-order logic is also consistent... In other words, if IFOL could prove the negation of LEM, then IFOL would be inconsistent and thus not useful in the first place. (Though in the case of propositional logic asked for in the original question, the Goedel translation of $P$ is equivalent to $\lnot\lnot P$.) $\endgroup$ Nov 23, 2021 at 22:41
  • $\begingroup$ @DanielSchepler Indeed. I edited my answer to include a sketch of a direct argument showing that the negation of LEM is not derivable in intuitionistic logic. $\endgroup$
    – Z. A. K.
    Nov 24, 2021 at 9:11
  • $\begingroup$ I don't understand how it is possible to prove $\lnot (A \lor \lnot A) \vdash A$ in intuitionistic logic. I agree that $\lnot (A \lor \lnot A) \vdash \lnot A$ is provable in intuitionistic logic, instead. $\endgroup$ Nov 24, 2021 at 21:15
  • 1
    $\begingroup$ Thanks for this excellent answer. Wish I could accept all of these answers. Clearly I have some things to learn about proof theory. $\endgroup$
    – Nat Kuhn
    Nov 25, 2021 at 2:59
9
$\begingroup$

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 ^_^

$\endgroup$
3
  • $\begingroup$ This is an excellent answer (+1). I'd like to learn more about Heyting Algebras and intuitionism in general. I have all the standard textbooks (I think); I just doubt I can get around to giving them the time they deserve. Topoi are exciting, too, and some of my first questions on MSE were about them. I'm not sure where I'm going with this comment so I'll stop here :) $\endgroup$
    – Shaun
    Nov 23, 2021 at 19:09
  • 1
    $\begingroup$ @Shaun, well now I've got butterflies, haha. And yeah, there's so much math worth learning, it's a real shame that we need to choose what we spend time with. I'm in a symmetric position to you with combinatorial group theory :P $\endgroup$ Nov 23, 2021 at 19:45
  • 1
    $\begingroup$ Thanks for this excellent answer. Wish I could accept all three great answers I've received! $\endgroup$
    – Nat Kuhn
    Nov 25, 2021 at 2:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.