Actual and Potential infinite

[Stephen G. Simpson]

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 aol.com> 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>