Dan, you keep saying you want to construct the real numbers. For most mathematicians, it means a way to enumerate them all, because the Axiom of Infinity or the last Peano Axiom concerning the successor function allow for tail recursion only! If you can do that, it means both logic and mathematics are inconsistent. Dedekind cuts are defined to be *cut* on R, forming (-oo, x) and [x, oo). They say nothing about the nature of continuum if you look at them carefully. The first interval simply says x is excluded, while the second says x is included. So, a point is a point. If it exists on both sides, then there is an overlap. So, it can only exist on one side. That's all! This is one of the most useless definitions I have seen, because it really says nothing about continuum. Plus, it does not even say what a point is.
Understanding starts with resolving paradoxes. One of the most intriguing intuition about continuum is that all of the following numbers are the same:
1) 1 2) 0.111... in base 2 3) 0.222... in base 3
They simply represent different rates of convergence. It means that if the gap keeps on decreasing monotonically, somehow the *final* point merges into its *adjecent* point. However, in continuum, an adjacent point is ill-defined. What is the number next to a number x, which I choose in R? Whatever x I choose, you cannot name its adjacent numbers?
1) There is no *final* point unless the list is *finite*. However, the notion of limit mysteriously solves this problem without explaining why. 2) The existence of an adjacent point is contradictory to the formal definition of continuum where whichever gap is chosen, a smaller gap can always be chosen from within. An adjacent point suggests the non-existence of such a gap at the *bottom* of the real line.
What is that limit that solves both problems together? Does a point exist in the continuum? Must we enforce the notion of an infinitesimal segment instead of a point derived from Dedekind cuts?
The puzzle must be solved for a clear understanding and therefore definition of the continuum we want to model.
Let's call this model CA for Continuum Axioms.
Once you have the axioms, you can start encoding CA with PA and PA with CA, just as you do with PDA (push-down automata) and CFG (context-free grammars). Unfortunately, if your CA correctly models the continuum, PA is not supposed to *encode* your CA, just as a PDA is not supposed to be able to encode a Turing machine.
I am just saying that you can approach this from the perspective of computer science if that's easier for you.
Can we have a *real* line as dense as Beth_w using the notion of infinitesimal segments?
Geometry can be as sick (or shall we say intriguing?) as set theories. They all get stuck at the same point anyway.