A question about finitism

[dennis.hamilton at acm.org]

From: FOM <fom-bounces at cs.nyu.edu> On Behalf Of Vaughan Pratt
Sent: Monday, February 13, 2023 22:24
To: Haim Gaifman <hg17 at columbia.edu>
Cc: fom at cs.nyu.edu
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.
 
[orcmid] …
 
(a)  Which of A, B, and  A --> B  can be stated in PRA?
 
(b)  Is A --> B a theorem of PRA?
 
Vaughan Pratt
[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.
 
 
 
 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20230217/620ffbdd/attachment-0001.html>