# Contrasting theorems in classical logic and constructivism

1. Is it possible there are examples of where classical logic proves a theorem that provably is false within constructivism? Is so what are some examples?

2. What are some examples of most contrasting theorems provable in these two logics that does not fall in 1.?

• Relevant, I think, are Brouwerian counterexamples. There are also no doubt many examples such as the following: Osvald Demuth, The differentiability of constructive functions (Russian, 1969). The MR review begins: "An increasing constructive function $[\cdots]$ on the constructive interval $[0,1]$ is given which $[\cdots]$ is nowhere differentiable." – Dave L Renfro Mar 28 at 8:27
• Brouwerian counterexamples are mostly good for convincing classical mathematicians that intuitionism makes no sense. – Andrej Bauer Mar 28 at 21:31

This is a very natural question, but as it happens one needs some more background to give a natural answer (is my humble opinion).

For clarity let me give a summary first indication:

As to your Question 1. : This is commonly thought of as not being possible in strict terms, because 'constructive mathematics' is usually interpreted as 'that part of alternative constructive mathematical theories which is compatible with classical mathematics.'

Broadly speaking, this interpretation of 'constructive mathematics' is known as BISH (from Bishop-style mathematics). BISH is seen as the common core of classical math (CLASS), intuitionistic mathematics (INT) and 'Russian' recursive mathematics a la Markov (RUSS).

Now if we include INT and RUSS in your term 'constructivism'. then the answer to question 1. is yes.

This because both INT and RUSS have additional axioms (compared to BISH) that are false classically. You could equally say that CLASS has an additional axiom compared to BISH (namely excluded middle) that is provably false in INT and RUSS.

Famous examples of conflicting theorems are:

a) All total functions from $$\mathbb{R}$$ to $$\mathbb{R}$$ are continuous (a theorem both in INT and RUSS)

b) The unit interval is compact in the Heine-Borel sense (a theorem both in CLASS and INT, but false in RUSS).

[Finally, if perhaps you mean only propositional first-order logic, then the answer is no again, because usually the term 'intuitionistic logic' is used to indicate that part of classical propositional logic which is valid constructively, which you can think of as `the part without excluded middle'.]

In the comment above, Brouwerian counterexamples are mentioned. Brouwerian counterexamples are explicit constructive examples where we can demonstrate that the classical 'solution' has insufficient constructive content (no general algorithm possible, or some other constructive deficiency). Often, Brouwerian counterexamples can be generalized to conflicting theorems in INT and/or RUSS. Brouwerian counterexamples are often useful in BISH to indicate that there can be little hope of constructivizing a certain classical theorem.

[Update 29 March | After your elucidation in the comments below, I feel I can give:]

Some remarks for Question 2:

a) An important example concerns axioms of choice. In constructivism (BISH, INT, RUSS) there are a number of choice axioms which may or may not conflict with each other and/or CLASS, depending on the precise phrasing and of course the intended logical strength.

In general, constructivists do not dismiss all forms of the idea that the statement for all $$x$$ there is $$y$$ such that $$P(x,y)$$ implies the existence of a choice function $$f$$ such that $$P(x, f(x))$$ holds for all $$x$$.

But the difference with CLASS (or between the others) can still be quite sharp, because of the very different interpretation of what is a 'meaningful' statement.

For a constructivist, 'meaningful' usually implies that we are talking about mathematical structures that can be constructed like (and therefore from !) the natural numbers $$\mathbb{N}$$, if we give ourselves enough time to do so. (Strict finitism is also a field of study in constructive mathematics, but since this is quite difficult it has not attracted many researchers).

In classical mathematics, a theory is often considered 'meaningful' already if we have good reason to believe that the theory is consistent. Whether the theory describes structures that we can actually build from scratch (viz. $$\mathbb{N}$$) is often not a matter of interest.

Strong intuitionistic axioms of choice sometimes expose this huge philosophical difference by leading to theorems which are false in CLASS, but sometimes they also lead to INT having the 'same' theorem as in CLASS (and you can only tell the difference by carefully interpreting the difference in meaning).

b) Another important example (also) concerns 'information' and 'interpretation'. Very very often, contradiction between CLASS and INT or RUSS can be meaningfully avoided by rephrasing. For example, by changing 'for all $$x$$' (CLASS) into 'for all $$x$$ for which we can determine whether $$x\geq 0$$ or $$x\leq 0$$' (INT), we might obtain the 'same' theorem.

This is imho a most salient point that Bishop added to Brouwer's views: why look for contradiction if you can rephrase for accordance?

However, imho it can also be very clarifying to study these contradictions. Usually one learns better how to rephrase for accordance when one has a clear idea where the conflict arises...

• This answer is spot on! I'd like to contribute the realizability topos given by infinite-time Turing machines as a further intriguing environment. Any topos has an "internal logic", but the one of this one is particularly challenges many mathematical intuitions shaped by classical logic. In this topos, there is no surjection $\mathbb{N} \to \mathbb{R}$ (as you would expect from CLASS), but there is an injection $\mathbb{R} \to \mathbb{N}$. This observation is due to Andrej Bauer. – Ingo Blechschmidt Mar 28 at 10:50
• @IngoBlechschmidt yes that is a nice addition. Am I correct in thinking that you mean an injection from Baire space $\mathbb{N}^{\mathbb{N}}$ into $\mathbb{N}$? Perhaps this also leads to an injection from $\mathbb{R}$ into $\mathbb{N}$ but I don't see this immediately, being poorly knowledged on toposes. – Franka Waaldijk Mar 28 at 12:20
• @Franka I meant $\mathbb{R}$, but indeed now that you say it I recall that Andrej proved it for $\mathbb{N}^\mathbb{N}$. Slides illustrating Andrej's proof are here (see slide 24/25). The argument easily adapts to $\mathbb{R}$, this is a fun exercise; if you want me to spell out the details, I'll gladly do so! – Ingo Blechschmidt Mar 28 at 12:36
• @VS. After your explanation I added some remarks on question 2. to my answer. The remarks are a bit generic, because specific examples would take too much detail (thus obscuring clarity for non-insiders). Hope you still can get the gist, if not I could try to specify a bit more. – Franka Waaldijk Mar 29 at 14:45
• This is partly a common situation in axiomatics... when we drop Euclid's fifth postulate, we get a weakening of Euclidean geometry. This weakening then allows us to add a non-parallelity axiom to obtain a non-Euclidean geometry which is contradictory to what we started with. Similarly intuitionistic first-order logic allows us to add non-classical axioms to obtain either full-blown INT or RUSS, which are contradictory to CLASS. Not adding these axioms gives us BISH, say. Historically Brouwer was by far the first (INT), which is why the terms intuitionistic and constructive get mixed. – Franka Waaldijk Mar 30 at 6:47

There are several ways one could interpret the word "constructivism" here, and the answer depends on what you meant by it.

Bishop-style constructivism is a generalization of Brouwerian intuitionistim, Russian constructivism, and classical mathematics. It is mathematics done without excluded middle (of course, you can still use excluded middle on those instances that you can prove to hold using other means) and general axiom of choice, but you still have countable choice. Thus, anything you prove in this setting is true in classical mathematics as well.

There are other forms of constructivism which are Bishop-style constructivism extended with additional principles and axioms. These additional principles often contradict classical logic, and so you get consequences that are classically false. Here are some examples:

In the internal language of the effective topos (an older name for this is Russian constructivism) the following are valid statements:

1. There are countably many countable subset of $$\mathbb{N}$$.
2. There is an increasing sequence in $$[0,1]$$ that has no accumulation point.
3. The Cantor space $$2^\mathbb{N}$$ and the Baire space $$\mathbb{N}^\mathbb{N}$$ are homeomorphic.
4. Every map $$f : [0,1] \to \mathbb{R}$$ is continuous.
5. There exists a continuous unbounded map $$f : [0,1] \to \mathbb{R}$$.
6. There is a covering of $$\mathbb{R}$$ by intervals $$(a_n, b_n)_n$$ with rational endpoints such that $$\sum_{k = 1}^n |b_n - a_n| < 1$$ for all $$n \in \mathbb{N}$$.
7. There is a subset $$S \subseteq \mathbb{N}$$ which is not finite and not infinite.
8. There exists an infinite binary rooted tree in which every path is finite.
9. The ordinals form a set, i.e., they are not a proper class. One has to be careful about how ordinals are defined and how to precisely understand the notions of "class" and "set", but these are technical details.

In the internal language of the realizability topos $$\mathsf{RT}(K_2)$$ (an older name for this is Brouwerian intuitionisism) the following statements are valid:

1. Every map $$f : X \to Y$$ between complete separable metric spaces is continuous.
2. Every map $$f : [0,1] \to \mathbb{R}$$ is uniformly continuous.
3. Every map $$f : \mathbb{R} \to \{0,1\}$$ is constant, or equivalently, if $$\mathbb{R} = A \cup B$$ and $$A \cap B = \emptyset$$ then $$A = \mathbb{R}$$ or $$B = \mathbb{R}$$.

There are many other examples. I recommend taking the effort to get used to these amazing new worlds of mathematics.

• What do the applied mathematicians say about these outrageous statements? – Monroe Eskew Mar 28 at 22:14
• I don't think they know about them, or at least I never got a reaction. There's a positive side to all of this, too. For example, in the effective topos everything is computable (in a precise sense). I'd imagine at least some applied mathematicians would appreciate that. In general, I find computer scientists will take anything that helps them solve their problems, even if it's outrageous. Mathematicians are more hung up on value judgements and respecting traditions. – Andrej Bauer Mar 28 at 23:18
• Oh, there's another topos (a model of intuitionistic bounded Zermelo set theory) that would interest applied mathematicians. In it all maps are differentiable and nilpotent infinitesimals exist, so you get to do analysis engineering-style, with $dx$'s and $dy$'s that are very small and whose squares are negligible. – Andrej Bauer Mar 28 at 23:23
• They are only antithetical to geometric and physical intuition under one understanding of "space" and "continuity" – the one you are aware of. It is entirely possible to develop different kinds of intuition (speaking from first-hand experience and having taught PhD students the alternatives) that let you "internalize" these statements. So, it's really the high-school teachers who determine what kind of intuitions the young minds will develop. In the current educational system there is only one kind. The resulting uniformity of thought gives the illusion of absolute truth. – Andrej Bauer Mar 29 at 9:27
• What would you say to the typical high school math teacher who says many of these statements can be disproven by drawing a picture? You can't really draw a discontinuous, total function, for example. No matter how accurately you try to draw it, you'll either leave a gap in the domain or make the pieces overlap, so that it's not a function. They are so antithetical to geometric and physical intuition. My physical intuition differs from yours. My physical intuition is that any time I see a discontinuous function, it's an idealized mathematical fiction, not physical reality. – Ben Crowell Mar 29 at 16:27