A question about finitism - reformatted

dennis.hamilton at acm.org dennis.hamilton at acm.org
Wed Feb 22 13:13:58 EST 2023

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

```