What is an example of a statment that one can prove in an Intuitionistic approch and cannot prove in the classic approch

Question

I know that there are things that one can prove using classic approch and not Intuitionistic approch (Using excluded middle will help you with a lot of proves). But are there any examples that works the opposite way ?

Answer 1

There are many systems of constructive mathematics. Some of them are compatible with classical logic in that all the theorems provable in these systems are classically true. Bishop's system has this property, for example.

Some systems are able to prove theorems that are not classically true. Some common examples of such theorems are:

• Every function from the real line to the real line is continuous.

• Every function from the real line to the natural numbers is constant.

• Every function from the natural numbers to the natural numbers is computable.

These arise as theorems and/or axioms in some systems, but such systems must necessarily have axioms or inference rules that are not classically valid.

There is another, intermediate option. In some other systems, it is not possible to prove any of the three bullets above, but any function that can be explicitly constructed in the system and proved to be a function will have the property.

One example is several systems of higher order Heyting arithmetic. For example, these systems do not prove that every function on the naturals is computable, but each function on the naturals that can be constructed and verified as a function in the system can be shown to be computable by a proof theory argument outside the system.