Finitism and primitive recursive arithmetic

[martdowd at aol.com]

FOM:
One can argue that Ackermann's function if finitist because there is a "self-evident" proof that the recursion terminates.  Here's an interesting paper on the subject, by Lawrence Paulson:  https://www.cl.cam.ac.uk/~lp15/papers/Formath/Ackermann.pdf

 Martin Dowd
 
 
-----Original Message-----
From: Richard Zach <rzach at ucalgary.ca>
To: fom at cs.nyu.edu
Sent: Wed, Dec 8, 2021 5:37 pm
Subject: Re: Finitism and primitive recursive arithmetic

 Thanks for the plug, Alasdair! Bill Tait has written a followup to his "Finitism" paper which, with discussion, is reprinted in his collected essays (The Provenance of Pure Reason). The original (without the added discussion) is on his website: 
  http://home.uchicago.edu/~wwtx/finitism.pdf He also has a more recent paper:
  Tait, William. "What Hilbert and Bernays Meant by “Finitism”". Philosophy of Logic and Mathematics: Proceedings of the 41st International Ludwig Wittgenstein Symposium, edited by Gabriele M. Mras, Paul Weingartner and Bernhard Ritter, Berlin, Boston: De Gruyter, 2019, pp. 249-262. https://doi.org/10.1515/9783110657883-015 It's unfortunately not on his website but you might be able to look at it on Google Books:
  https://books.google.ca/books?id=60DEDwAAQBAJ&lpg=PR1&pg=PA249#v=onepage&q&f=false If I'm not mistaken, he discusses something very much like the idea you propose (the Sieg/Ravaglia argument). FWIW I agree with Bill that the conceptually best analysis of what Hilbert *should have* meant by "finitism" is PRA. My "scepticism" about Tait's proposal only concerned the historical question of whether Hilbert et al. ever used methods that went beyond PRA in his proof theory. I think Bill agrees with me on the historical question.
  -RZ
  On 2021-12-08 10:21, Alasdair Urquhart wrote:
  
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
 
 
 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20211210/250289ca/attachment-0001.html>