Showing changes from revision #1 to #2:
Added | Removed | Changed
Disambiguation page
There are many different types which are called Dedekind real numbers in the literature. All of them involve the use of Dedekind cuts?Dedekind cut s in a dense integral subdomain of the rational numbers in their definition, and they differ based upon which definitions of a Dedekind cut are used. These include:
two-sided Dedekind real numbers?, which is defined using Dedekind cuts, which are defined using the type of all prepositions in a universe.
lower Dedekind real numbers?, which is defined using only lower Dedekind cuts.
upper Dedekind real numbers?, which is defined using only upper Dedekind cuts.
The following types are defined as above but uses Sierpinski space instead of the type of all prepositions in a universe to define Dedekind cuts:
predicative two-sided Dedekind cut structure real numbers?
predicative lower Dedekind cut structure real numbers?
predicative upper Dedekind cut structure real numbers?
The following real number types are defined using the type of all propositions in a universe, so that the real number types form a (large) frame (in the next universe in the hierarchy):
two-sided extended Dedekind cut structure real number?
lower extended Dedekind cut structure real number?
upper extended Dedekind cut structure real number?
The following real number types are defined as above but uses Sierpinski space instead of the type of all prepositions in a universe to define Dedekind cuts, so that the real number types form a $\sigma$-frame in the same universe rather than a large frame in the next universe in the hierarchy.