finitism and primitive recursive arithmetic

[martdowd at aol.com]

FOM:
I was just reading
 Takeuti's Well-Ordering Proof: Finitistically Fine?
  by Eamon Darnell and Aaron Thomas-Bolduc,
 philsci-archive.pitt.edu/15160/1/Takeuti.pdf
They mention Tait's thesis that PRA exhausts finitistic methods.

It occurred to be that the terms of PRA can be augmented by adding a function,
which is the universal function for primitive recursive functions.  If
a nice extension of PRA existed allowed proving facts about this,
wouln't this still be finitistic?

One possibility might be to add some version of Hoare's axioms to Meyer-
Ritchie loop programs.

Martin Dowd

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20211207/95fbc690/attachment-0001.html>