Actual and Potential infinite

[JOSEPH SHIPMAN]

ACA_0 doesn’t require actual infinity in my book, because any arithmetical consequence of it can be proven from ZF without using the axiom of infinity, right?

— JS

Sent from my iPhone

> On Feb 7, 2023, at 1:26 PM, Stephen G. Simpson <sgslogic at gmail.com> wrote:
> 
> 
> 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/523a78a4/attachment.html>