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

[Joao Marcos]

Timothy Y. Chow wrote:
>
> There is of course a long tradition in philosophy of distinguishing
> between "potential infinity" and "actual infinity."  In modern
> mathematics, this distinction doesn't seem to exist.  The closest thing to
> "potential infinity" seems to be an axiomatic system that lacks anything
> that could be identified as an explicit "axiom of infinity," yet admits
> only (actually) infinite models.  (PA would be an example.)  But for
> example, I've never seen anyone define two separate axioms and declare one
> of them to be an "axiom of potential infinity" and the other an "axiom of
> actual infinity."
>
> I'm wondering if anyone can come up with (or has already come up with)
> candidates for two such axioms, the former demonstrably weaker than the
> latter, such that the consistency of PA can be proved using only the
> "axiom of potential infinity."  Doing this might be pleasing to those who
> not only perceive an important distinction between potential and actual
> infinity but go so far as to reject the latter while accepting the former.

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?

Joao Marcos