Contrasting theorems in classical logic and constructivism

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.

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