A question about finitism
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>
More information about the FOM
mailing list