Are the computable reals finitary? In the comment thread of an answer, I said:

The computable numbers are based on the intuitionistic continuum, and are not finitary. 

To which T.. replied:

Computable numbers are not based on the intuitionistic continuum.

This disagreement contains, I think, a good example of a philosophical question: are the computable reals within the scope of finitistic mathematics?
References


*

*Bendegem, 2010, Finitism in Geometry

*Edalat, 2009, A computable approach to measure and integration theory

*Zach, 2001, Hilbert's Finitism

*Zach, 2003, Hilbert's Program
 A: A real number $r$ is defined to be computable if there is an algorithm that, given any natural number $n$, will produce a rational number within distance $1/n$ of $r$. Thus each individual computable number is defined using a finite amount of information (the algorithm). On the other hand, there is a well-known intuitive sense in which an arbitrary real number can contain an infinite amount of information. In this sense, computable real numbers are finitary in a way that arbitrary real numbers are not. 
The definition of a computable real number can be stated in either classical mathematics or in intuitionistic mathematics. Nothing in the concept of a computable real number ties you to one logic or the other. 
A: The following are unrelated concepts:


*

*Finitism

*The "intuitionistic continuum" (does that mean Weyl's book? the real numbers as defined in Bishop's book on constructive analysis?)

*Computable real numbers
For example, you can read the definition of computable real numbers under a classical or an "intuitionistic" interpretation of the words, and they will differ as to whether "1 if Goldbach conjecture is true and 2 if it's false" is a computable real number.  But the theory of computable reals will make sense in both environments.
A: Depends on what you exactly mean by finitary. A computable real has a finite description (a Turing Machine), so it is a finite object. 
But many properties of computable real numbers are not finitary.
We can develope an interesting amount of analysis in very weak arithmetic theories (see this), theories which are much weaker PRA (which is often associated with Hilbert's finitism).
A: I'm not so sure about the "finitary" definition, but I'm fairly certain that the class of partially computable functions (those for which algorithms can be devised) is countable. I'd thus conjecture that the computable reals are, at the very least, countable. Can anybody confirm or deny this, and/or relate what I have said to this concept of "finitary"?
