Re: Cantor set/cantor dust and constructivism

[Peter Freyd <pjf@saul.cis.upenn.edu>]

The question is: "From a constructivist viewpoint though, can we ever
realize the actual object which is infinite?"

Unless you specialize to decidable objects (excluded middle for
equality) then there is no easy way to _avoid_ infinite objects.

One may get a hint of this from the following example: in the category
of  N-sets (sets with a distinguished self-map) let  A  be the
two-element set in which the distinguished self-map has a unique
fixed point. In Cats and Allegories (1.925) we point out that  A^A,
the object of self-maps of  A, falls apart as a coproduct (disjoint
union) of continuously many  N-sets. Hence if one takes the set of
equivalence classes of  A^A, where the equivalence relation is the
double-negation of equality, one obtains a discrete set (it has
trivial N-action) whose cardinality is the continuum.

But that's just a hint.

Consider the following theorem for topoi. Let  T  be the initial
object in the category of topoi and logical morphisms. _No axiom of
infinity._ Let  1  be the terminator in  T.  Let  Omega  be its power
object. Let  P  be  Omega^Omega, the object of self-maps on  Omega.
There's a subobject, M, of  P  on which we may define the structure of
a rig (a ring without negation) that mimics the natural numbers. In
particular the set of global sections, that is, maps from  1  to  M
with its inherited rig structure, is isomorphic to the standard natural
numbers.

Because the global sections can be misleading in an arbitrary topos
it's worth pointing out that  M  mimics the natural numbers even from
an internal point of view. For instance given any pair of polynomials,
f(x_1,...,x_n), g(x_1,...,x_n)  with natural-number coefficients the
the first-order sentence

  \exists_{x_1,...,x_n\in M}   f(x_1,...,x_n) = g(x_1,...,x_n)

is satisfied in  T  iff it is satisfied in the standard natural
numbers.

An elaboration of this argument allows us to construct a topos-object
in  T  whose topos of global sections is isomorphic to the free topos
with natural-numbers-object. And, as for  M, an equation in the theory
of topoi is internally true for this internal topos iff it is true for
the free topos with NNO.

Lest one think I'm butting up against the consistency proof, the truth
value in  T  of  0 = 1  in  M  is not totally false. (That is, M  is
"somewhat inconsistent" from the internal point of view.) From the
external point of view, though, the two maps from the terminator to  M
that name  0  and  1  are not equal (from the internal point of view
their equalizer is non-trivial). In particular we can find  f,g  so
that the first-order sentence above has no standard solutions but is
not totally false in  T.

The slogan: once you've given up excluded middle there's no gain in
giving up the axiom of infinity.