Here are two well known facts, which put together leave me confused.

First, it's well known that intuitionistic logic is the logic of constructive mathematics. From every intutionistic proof, you can extract an algorithm which will compute the witness to that theorem (i.e., the famous "existence principle" of intutionistic logic).

Second, it's also well-known that topologies give rise to models of intuitionistic mathematics. We can equate propositions with open sets, and then the fact that a topology is a Heyting algebra gets us off to the races. (Caveat: this is an oversimplification.)

In fact, you can get pretty far with the dictionary "computability is continuity" -- which is precisely what puzzles me!

Intuitionistically, we can construct the real numbers pretty much as usual, eg via Cauchy sequences, which can be viewed as functions $\mathbb{N} \to \mathbb{Q}$ subject to the usual conditions. Now recall that classically, the only continuous functions $f : \mathbb{R} \to \mathbb{Z}$ are the constant functions. So according to this dictionary, we should not expect to give an intuitionistically valid function which computes the integer part of a real number.

So far, everything makes sense. For example, the Cauchy sequence $0, 0.9, 0.99, 0.999, \ldots$ has $1$ as its limit, but given a black-box $f : \mathbb{N \to \mathbb Q}$, we can't tell that it's this sequence without looking at every $f(n)$ -- which is obviously uncomputable.

However, suppose that we have in our hand an actual computer program of type $\mathbb{N} \to \mathbb{Q}$ (say, in Haskell), which we happen to know represents a Cauchy sequence. We can actually run this program, and use some prefix of the Cauchy sequence to print something close to the integer part of the real to the computer screen. This operation obviously isn't a *function* on reals, since it can give different results for different representations of the same real. For example, our program might print "1" for the Cauchy sequence $1, 1, 1, \ldots$, and "0" for the Cauchy sequence "$0.9, 0.99, 0.999, \ldots$". But equally obviously this a perfectly sensible *computer program* to write.

So that's my question: what *is* this operation, and how can we axiomatize its logical behavior? (What kind of crazy gadget doesn't respect equality!?)

2more comments