[FOM] axioms for potential infinity and for actual infinity?

[Maarten McKubre-Jordens]

Joao Marcos wrote:

> Hummm... what if one replaced ZF's *Axiom of Infinity*, that
> postulates the existence of inductive sets, by an axiom that
> postulated the existence of
> sets equipped with endofunctions that are injective but not
> surjective?  It is well-known that the latter sets (known as
> *Dedekind-infinite*) are infinite in the usual sense, while proving
> the converse demands some extra technology, such as AC? (countable
> choice).
>
> This is all standard, but I wonder if anyone has tried to use it as a
> way of rescuing the age-old philosophical distinction between actual
> and potential infinity.  No doubt, if Dedekind-infinite is to mean
> "actual", to give the traditional Axiom of Infinity a distinct
> "potential" flavor it might make sense to move first to a *predicative
> version of ZF* (which will often weaken also the powerset axiom to
> some sort of "axiom of exponentiation"), so that the "existence"
> postulated by the axiom is given a constructive reading.  Does anyone
> know if *infinite* implies *Dedekind-infinite* in Constructive ZF with
> Dependent Choice?

I don't know if this is a help, but there's a paper from Lubarsky and Rathjen where they construct a Kripke model that shows that, without Dependent Choice, the Dedekind reals form a proper class whereas the Cauchy reals form a set. The equivalence of the latter two in Bishop-style constructive mathematics can be explained by the acceptance of Dependent Choice in that theory. The reference is:

Robert S. Lubarsky & Michael Rathjen, 'On the constructive Dedekind reals', Logic and Analysis 1 (2):131-152 (2008).

Based on that, my guess would be that infinite does imply Dedekind-infinite provided one has Dependent Choice.

Best,
Maarten


This email may be confidential and subject to legal privilege, it may
not reflect the views of the University of Canterbury, and it is not
guaranteed to be virus free. If you are not an intended recipient,
please notify the sender immediately and erase all copies of the message
and any attachments.

Please refer to http://www.canterbury.ac.nz/emaildisclaimer for more
information.