A question about finitism

[Vaughan Pratt]

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.

If someone has answered it in the meantime, my apologies for failing to
recognize it as such.

In any event, now that I know that PRA, with proof-theoretic ordinal
omega^omega, is the criterion for finitism proposed by my
great-great-grand-advisor Thoralf Skolem in reaction to Russell and
Whitehead's *Principia Mathematica* (h/t to Bill Tait for his clarifying
expositions on that proposal)*,* I have the following sharpening of my
question.

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

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

Vaughan Pratt
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20230213/ab150742/attachment-0001.html>