A question about finitism - reformatted

[dennis.hamilton at acm.org]

It has been kindly brought to my attention that certain forms of email 
messages do not transit through the list server and subscriber's email readers 
in good form.

Here is my most-recent post on FOM in plain-text with quotation fences (">"). 
This is imperfect - only the first line of paragraphs have the fence.  The 
insertion of in-paragraph line breaks is not my doing.

From:  Vaughan Pratt
Sent: Monday, February 13, 2023 22:24
Subject: Re: A question about finitism

 > My first contribution to the present thread on finitism included a question 
about two propositions about non-empty linear orders L.  Proposition A is "L 
has no greatest element", while proposition B is "L is infinite".   My 
question was whether the proposition  A --> B was finitistic in some sense.
 .

> (a)  Which of A, B, and  A --> B  can be stated in PRA?

 > (b)  Is A --> B a theorem of PRA?

[orcmid]
I can't see how the specified A -> B can be a theorem in PRA, I don't think 
there is any way to express proposition B with PRA.  Also, because PRA lacks 
qualifiers, it is not clear to me that A is expressible either, since you have 
to express the non-existence of a number that no number exceeds.

After huddling with Bing Chat on a matters of finitism and already reading the 
relevant Wikipedia articles, I can confirm that modus ponens is a rule of 
deduction in PRA.  I love that the 
<https://en.wikipedia.org/wiki/Primitive_recursive_arithmetic> account points 
out that there is a "countably infinite number of variables x, y, z, . ."  So, 
I am not the only one who has trouble demonstrating a comfortable classic 
finitist stance.

Personally, I have no interest in denying set theory and transfinite entities, 
such as N taken as the Peano Numbers aggregated in their entirety.  I simply 
don't want to rely on it and infinities generally when it is unnecessary.  I 
don't give up structural induction though.

I am also happy that I can accept general recursiveness (because Turing and 
Ackermann's function), although we're stuck that a UTM, taken as a function, 
is not going to be total.  So computability and computation models live at the 
boundary.  So be it and no farther.