The Question
I'm looking for a possibility to somehow proof the "essence" of Cantor's diagonal argument within a recursive first-order theory which is satisfied by the reals (better: within a theory of one is saying that its standard model are the reals).
With "essence" is meant, that I want to express within the theory that the universe (i.e. the reals via standard interpretation) is uncountable.
The motivation behind this is to demonstrate Skolem's paradox.
As this is something I would like to explore, this question can be seen as a literature/reference request.
Some Notes
Besides the technical problems of defining functions (or sequences, tupels, ...) within the theory of complete ordered fields I'm facing Gödel's barrier. Since this very theory is complete it should not be able to express something like $x \in \mathbb{N}$ or such, which seems essential to express uncountability. At least there has to be some parts of $\mathbb{N}$ which one is able to express if stating uncountability. This leads to several possibilities:
- Change the theory (to some which is satisfied by the reals, recursive, maybe just extend the language by a relation symbol $N$?),
- express "the universe is uncountable" in another way, or
- prove that it is in general not possible
and to the alternate question: Is it possible to express uncountability in a way using $\mathbb{N}$ to a minimal amount such that the incompleteness theorem isn't effective?
Unfortunately I'm somewhat new to that field and insofar I lack knowledge.
Thanks for any hints, literature or ideas.
The first-order theory that has the Reals as it's standard model is the theory of Real Closed Fields (RCF). But its not a categorical theory, which means that there are many countable, uncountable, and models of any cardinality (Lowenheim-Skolem theorem).
In order to recreate a instance of Skolem Paradox, we would need a language powerful enough to state "there is an uncountable set" (and that's of course is enough to say that the universe is uncountable) in a countable model. But the theory of RCF is not that powerful.
You could, of course, add axioms to the theory of RCF that would express the existence of a (proper) set that satisfies some PA-like axioms and call that set $\omega$. With that in hand it's possible to define the property of being "uncountable" in your theory. And of course, there would be countable models of this RCF+PA. That, I think, would be a minimal instance of Skolem Paradox in a recursive first order theory.