TWO (OR THREE) NOTIONS OF FINITISM

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 J^.2 based on the algebra of lower elementary functions. The extension of this algebra to Grzegorczykʹs class e2 can be justified by means of an additional finitistic choice principle, thus obtaining a second equational theory T^. It is unknown whether J^a is strictly stronger than since £2 may 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 Tg that may be incomparable to Tgi (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.