How can some statements be consistent with intuitionistic logic but not classical logic, when intuitionistic logic proves not not LEM?

Question

I've heard that some axioms, such as "all functions are continuous" or "all functions are computable", are compatible with intuitionistic type theories but not their classical equivalents. But if they aren't compatible with LEM, shouldn't that mean they prove not LEM? But not LEM means not (A or not A) which in particular implies not A - but that implies (A or not A). What's gone wrong here?

Answer 1

If $A$ is a sentence (ie has no free variables), then your reasoning is correct and in fact $\neg (A \vee \neg A)$ is not consistent with intuitionistic logic.

However, all the instances of excluded middle that are contradicted by the statements "all functions are continuous" and "all functions are computable" are for formulas of the form $A(x)$ where $x$ is a free variable. To give an explicit example, working over Heyting arithmetic (HA), let $A(n)$ be the statement that the $n$th Turing machine halts on input $n$. Then, it is consistent with HA that $\forall n\;A(n) \vee \neg A(n)$ is false. That is, $\neg (\forall n \; A(n) \vee \neg A(n))$ is consistent with HA, and is in fact implied by $\mathsf{CT}_0$ (essentially the statement that all functions are computable). Note that even in classical logic this doesn't directly imply $\neg A(n)$, which would be equivalent to $\forall n \; \neg A(n)$. What we could do in classical logic is deduce $\exists n \; \neg (A(n) \vee \neg A(n))$ and continue as before, but this does not work in intuitionistic logic.

Answer 2

This is an expansion of Henry's comment. If we don't add any additional axioms, intuitionistic logic (by which I mean all the standard systems such as HA, IZF, etc.) is compatible with the law of the excluded middle LEM, but does not prove LEM. This is a useful fact to know when learning about these logics - they don't prove anything that is classically false, although there are some things that are classically provable that they cannot prove.

Now, if there is a sentence $\lnot \phi$ that is classically provable but not provable in some intuitionistic system $I$, then $\phi$ is classically disprovable, so $\lnot \phi$ has no classical model. But since $\lnot \phi$ is not provable in $I$, $\phi$ is consistent with $I$ (because a proof of a contradiction from $\phi$ is exactly a proof of $\lnot \phi$ in an intuitionistic system). So by the appropriate completeness theorem for $I$, there will be a model of $I$ satisfying $\phi$, but that model must necessarily be nonclassical.

Concrete examples of $\phi$ that have this property are "every function from $\mathbb{N}$ to $\mathbb{N}$ is computable" and "every function from $\mathbb{R}$ to $\mathbb{R}$ is continuous". These are disprovable classically, but not intuitionistically. How is that? The way to understand it is to exame the classical disproof.

To prove "not every function from $\mathbb{N}$ to $\mathbb{N}$ is computable" we would say to define a function $f$ so that, for each $n$, if the $n$th computable function halts with output $m$ on input $n$ then $f(n) = m+1$, and $f(n) = 0$ otherwise. Then it is immediate that $f$ is not computable. In intuitionistic logic, if there was an $f$ with the property, we could still prove it is not computable. But the definition just given is not a sound definition in intuitionistic logic. It is possible to show for many intuitionistic systems that they do not prove "for all $n$, the $n$th computable function either halts on input $n$ or does not halt on input $n$". So the definition of $f$ by cases fails, because we cannot prove that the cases in the definition are exhaustive. The problem is not that $f$ is not a functional relation, it's that $f$ may not be a total function if we interpret the definition in a nonclassical model.

Similarly, the easiest way to make a discontinuous function on the reals is to define it by cases, e.g. $g(0) = 1$ and $g(x) = 2$ for $x \not = 0$. We cannot prove intuitionistically that there is no function $g$ with that property, because there are classical models of intuitionstic systems where there is such a function. But the definition by cases is only successful in models that satisfy $(\forall x\in\mathbb{R})[x = 0 \lor x \not = 0]$, and it turns out there are nonclassical models of intuitionistic systems that do not satisfy that sentence. In such models, we cannot define the function $g$, in fact.

Answer 3

I think you're confusing two things here: intuitionistic logic and finitistic (intuitionistic) mathematics. Intuitionists are driven by the philosophy that Truth should be equated with provability and Falsehood should be equated with refutability.
Hence, intuitionistic logic is characterized by rejecting several classical tautologies such as LEM (because there may be statements which are neither provable nor refutable), Double Negation Elimination (to refute that a proposition is refutable doesn't prove it is provable), or $\neg \forall xP(x) \leftrightarrow \exists x \neg P(x)$ (because for the intuitionists an existence proof must be constructive). Note, however, that this doesn't commit the intuitionist to claiming that there is a counterexample to LEM, i.e. just because LEM may not always be 'true' (provable) doesn't mean there is (we can construct) a counterexample.
Finitistic mathematics on the other hand is characterized by the rejection of a 'completed' infinity. It only acknowledges (possibly infinite) objects that can be computed to arbitrary precision. So in a sense finitistic mathematics rejects non-recursive sets and proofs involving diagonal arguments: For example Cantor's proof that $\Bbb R$ is uncountable is not acceptable in finitistic mathematics, because it implements a construction of an element by 'infinite inspection' (by complete inspection of an infinite list). In finitistic mathematics "all real functions are continuous" is true because $\Bbb R$ only consists of the constructible elements, which are countable, and for any countable set of pairs (x,y) there is a continuous map with $f(x)=y$.
Now intuitionistic logic doesn't imply finitistic mathematics, nor is it refuted by classical logic, but it usually comes with the philosophy that grounds intuitionistic logic.