Actual and Potential infinite

Stephen G. Simpson sgslogic at
Tue Feb 7 13:26:12 EST 2023

Many examples for your question 2) are in my book "Subsystems of Second
Order Arithmetic."  For instance, the theorem "every continuous function
from the unit cube into itself has a fixed point" requires only potential
infinity, in the following "reasonable" sense: it is provable in (a
"reasonable" conservative extension of) WKL_0, which is itself conservative
over PRA for "finitistically meaningful" sentences.  Here by
"finitistically meaningful" I mean Pi^0_2.  And, the theorem "every
countable Abelian group has a divisible closure" requires actual infinity,
in the sense that it reverses to ACA_0.  Or, if you think that ACA_0
doesn't require actual infinity, try changing the example to "every
countable Abelian group is the direct sum of a divisible group and a
reduced group."  This reverses to Pi^1_1-CA_0, which is much stronger.

Your question 1) is a different matter.

On Mon, Feb 6, 2023 at 8:16 AM JOSEPH SHIPMAN <joeshipman at> wrote:

> Most of the discussion that is going on about “actual” and “potential”
> infinite does not seem to involve any theorems, so let me ask a couple of
> questions that focus on mathematical practice.
> 1) Is there any proposition statable in the language of first order
> arithmetic, which is a theorem of ZF but not of PA, which can be said not
> to require “actual infinity” to prove?
> 2) Can you name two theorems T1 and T2 statable in the language of
> analysis (second order arithmetic), whose *statements* are of the same
> logical type, such that T1 requires “potential infinity“ but not “actual
> infinity”, but T2 requires “actual infinity”, for some reasonable meaning
> of “requires”?
> I am struggling to understand how this discussion, when reduced to
> questions of what can be proven, is about anything other than the cut point
> in the hierarchy of logical strength that appears between PA and PA+Con(PA).
> — JS
> Sent from my iPhone
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20230207/09d33c72/attachment-0001.html>

More information about the FOM mailing list