TWO (OR THREE) NOTIONS OF FINITISM
Mihai Ganea · The Review of Symbolic Logic · 2010
Finitism is given an interpretation based on two ideas about strings (sequences of symbols): a replacement principle extracted from Hilbert’s work and a counting principle inspired by Tait. These principles are used to justify an equational arithmetic ${\cal T}_{{\cal L}^2 } $ based on the algebra of lower elementary functions. The extension of this algebra to Grzegorczyk’s classɛ2can be justified by means of an additional finitistic choice principle, thus obtaining a second equational theory ${\cal T}_{{\cal E}^2 } $ . It is unknown whether ${\cal T}_{{\cal E}^2 } $ is strictly stronger than ${\cal T}_{{\cal L}^2 } $ sinceɛ2may coincide with the class of lower elementary functions. If the objects of arithmetic are taken to be binary numerals instead of tally numerals, then it becomes possible to provide a finitistic justification for a theory ${\cal T}_B $ that may be incomparable to ${\cal T}_{{\cal E}^2 } $ (neither of the two includes the other). I conclude by suggesting that the equational theory of Kalmar elementary functions is a strict upper bound for finitistic arithmetic.