[FOM] Potential and Actual Infinity

[WILLIAM TAIT]

Some remarks on the discussion of the distinction between the actual and potential infinite. 

An actual infinity is an infinite object, (representable by us as an infinite set, as e.g. Joe Shipman notes).

John Bell has shown how the potential infinite can be 'represented' by an object; but the historical notion of a potential infinity (i.e. Aristotle's) is not of an object, but of a species of objects together with an operation for constructing more and more objects of the species. (In John's example, the objects in the topos E are in fact actual infinities: \omega sequences of maps. It is only by restricting the language in which we speak of them to the internal language of the topos that they are merely 'potentially infinite'.)

Panu Raatikainen (3/4) has raised a point that has always troubled me. Both Hilbert and the early intuitionists have associated commitment to the actual infinite with the use of classical logic, so that, for example, the use of quantification over the integers combined with classical logic commits one to the the set of integers as an actual infinity. I would like someone to explain why this is the same notion of actual infinity as Aristotle's. (One might ask, too, whether quantification over the integers using intuitionistic logic commits one to the actual infinite---and why.)

Giovanni Sambin (\pi) refers to Gentzen's consistency proof for PA using induction up to \epsilon_0 as an example of a consistency proof for that system that does not employ the actual infinite. Certainly Gentzen was also of that view and indeed argued for it. But does it really avoid the actual infinite? In the coding of the ordinals up to \epsilon_0 by natural numbers, let m be the code for \omega. As a natural number, m is certainly finite; but in its role as representative of \omega, it has infinitely many predecessors. (Of course, the form of induction on \epsilon_0 used in Gentzen's proof is the weak free-variable form: having established for a primitive recursive A

A(0) and (A(f(x))--> A(x) (where f satisfies the condition f(x) =0 or f(x) < x, < being the \epsilon_0 ordering)

we can conclude A(x). But it is still not clear to me how the argument avoids the actual infinite. (One needs this form of induction for a wide class of functions f.) Or better: I am unsure what the claim means that Gentzen's argument avoids the actual infinite.

Best wishes to all,
Bill