Finitism and primitive recursive arithmetic

[Alasdair Urquhart]

Richard Zach has given a detailed logical and historical
analysis of this question in his 2001 Berkeley doctoral thesis.
It's available at Richard Zach's website.

Zach expresses scepticism about Tait's proposal.  If you are interested
in this question, I strongly recommend his dissertation.


On Tue, 7 Dec 2021, martdowd at aol.com wrote:

> 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