Actual and Potential infinite

[Stephen G. Simpson]

 Yes, ACA_0 is conservative over PA.  But Bill Tait in his papers argues
that Hilbert's finitism is embodied by PRA, not PA or any stronger system.
So if you agree with Tait, then you have to say that the potential/actual
dividing line is way beyond the finitism/infinitism dividing line.   Right?

On Tue, Feb 7, 2023 at 12:34 PM JOSEPH SHIPMAN <joeshipman at aol.com> wrote:

> 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/ebde555b/attachment.html>