Intuitionistic Real Analysis?

Question

It seems like the following argument is in some sense the basis of real analysis:

If $\forall\epsilon>0,\;\; d(x,y)<\epsilon$ then $x=y$.

But in order to prove this statement, wouldn't that require contradiction and double negation? So this principle doesn't seem very intuitionistic... I know many computer scientists say tongue and cheek that "the real numbers don't exist", but this doesn't seem very productive for general proof verification system goals for working mathematics.

So my questions are these: is this principle taken as an axiom on its own in an intuitionistic setting? Does taking this as an axiom lead to something catastrophic like introducing principle of excluded middle globally? What are work-around's to this?

Answer 1

In most constructive systems of analysis, there are two kinds of equality.

The first is "intensional" equality. If you imagine that two real numbers are given by computer programs, the numbers are equal in this sense if they have the exact same program. In particularly, if I "give you" two numbers, you can tell immediately if they are intensionally equal or not.

The second is "extensional" equality. Two real numbers are defined to be equal in this sense if, for every $\epsilon > 0$, the distance between the numbers is less than $\epsilon$. Given two numbers, there may be no way to tell if they are extensionally equal. So extensional equality is really just an equivalence relation, although it does act something like "equality".

This way of working is very common in constructive mathematics: many objects come equipped with an equivalence relation of "extensional equality", which is often not decidable.

Actually, in constructive settings it can be more convenient to define what it means for two numbers to be not extensionally equal. Two numbers are separated if there is a natural number $n$ such that the distance between the numbers it at least $1/n$. This is a more useful definition, constructively, because it has an existential quantifier. The direct negation of "not extensionally equal" would only have a negated universal quantifier, which cannot be converted to an existential quantifier in many constructive systems.

Because we don't have the law of the excluded middle, there end up being three cases for the relationship between two reals in a typical constructive system:

• (We know that) they are extensionally equal
• (We know that) they are separated
• We do not know whether they are extensionally equal or whether they are separated.

What classical logic does is to eliminate the third option, because classically "extensionally equal" is equivalent to the negation of "separated".

Answer 2

I don't have enough reputation to comment. but hopefully this is enough for you to answer your question.

I believe page 6 of this book on constructive analysis should clear some things up. constructive analysis

In short, constructivists ( or intuitionists) use a different definition of the Real numbers. I believe a common one is given in the link, where they are defined as regular sequences. See the link to see what that means. Note: It is somewhat similar to what you stated, though instead of circularly in terms of real numbers $\epsilon$, it is defined in terms of integers, similar to the archimedean property we are used to of the reals (or rationals).