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



Contrasting theorems in classical logic and constructivism
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... 


