Abstract:
We consider a quantifier-free induction schema and the least element principle in the language of elementary arithmetic enriched by a free function symbol $f$. Some stronger, iterated versions of these schemata are also considered. We show that the iterated induction schema does not prove the existence of a maximum of $f$ on every finite interval. A similar result is obtained for the noniterated least element principle. At the same time, already the doubly iterated least element principle for quantifier-free formulas proves the existence of a maximum of $f$. We also obtain additional results on the relationships between the two schemata, and outline their connections with the induction schema and the least element principle for decidable relations.