dennis.hamilton at acm.org dennis.hamilton at acm.org
Fri Feb 17 15:56:51 EST 2023

```
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>
```