Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions reals.tex
Original file line number Diff line number Diff line change
Expand Up @@ -3035,9 +3035,9 @@ \section{The surreal numbers}
\index{Abstract Stone Duality}%
This is a (restricted) form of simply typed $\lambda$-calculus with a distinguished object $\Sigma$ which classifies open sets, and by duality also the closed ones. In~\cite{BauerTaylor09} you can also find detailed proofs of the basic properties of arithmetical operations.

The fact that $\RC$ is the least Cauchy complete archimedean ordered field, as was proved in \cref{RC-initial-Cauchy-complete}, indicates that our Cauchy reals probably coincide with the Escard{\'o}-Simpson reals~\cite{EscardoSimpson:01}.
\index{real numbers!Escardo-Simpson@Escard\'o-Simpson}%
It would be interesting to check\index{open!problem} whether this is really the case. The notion of Escard{\'o}-Simpson reals, or more precisely the corresponding closed interval, is interesting because it can be stated in any category with finite products.
The fact that $\RC$ is the least Cauchy complete archimedean ordered field, as was proved in \cref{RC-initial-Cauchy-complete}, indicates that our Cauchy reals probably coincide with the Escard{\'o}--Simpson reals~\cite{EscardoSimpson:01}.
\index{real numbers!Escardo--Simpson@Escard\'o--Simpson}%
It would be interesting to check\index{open!problem} whether this is really the case. The notion of Escard{\'o}--Simpson reals, or more precisely the corresponding closed interval, is interesting because it can be stated in any category with finite products.

In constructive set theory augmented by the ``regular extension axiom'', one may also try to define Cauchy completion by closing under limits of Cauchy sequences with a transfinite iteration.
It would also be interesting to check whether this construction agrees with ours.
Expand Down