Geodesic
Quantifier-Free Induction Schema and the Least Element Principle
Informatics and Automation, Mathematical logic and algebra, Tome 242 (2003), pp. 59-76.

Voir la notice de l'article provenant de la source Math-Net.Ru

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. 
@article{TRSPY_2003_242_a4,
     author = {L. D. Beklemishev},
     title = {Quantifier-Free {Induction} {Schema} and the {Least} {Element} {Principle}},
     journal = {Informatics and Automation},
     pages = {59--76},
     publisher = {mathdoc},
     volume = {242},
     year = {2003},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/TRSPY_2003_242_a4/}
}
TY  - JOUR
AU  - L. D. Beklemishev
TI  - Quantifier-Free Induction Schema and the Least Element Principle
JO  - Informatics and Automation
PY  - 2003
SP  - 59
EP  - 76
VL  - 242
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/TRSPY_2003_242_a4/
LA  - ru
ID  - TRSPY_2003_242_a4
ER  - 
%0 Journal Article
%A L. D. Beklemishev
%T Quantifier-Free Induction Schema and the Least Element Principle
%J Informatics and Automation
%D 2003
%P 59-76
%V 242
%I mathdoc
%U http://geodesic.mathdoc.fr/item/TRSPY_2003_242_a4/
%G ru
%F TRSPY_2003_242_a4
L. D. Beklemishev. Quantifier-Free Induction Schema and the Least Element Principle. Informatics and Automation, Mathematical logic and algebra, Tome 242 (2003), pp. 59-76. http://geodesic.mathdoc.fr/item/TRSPY_2003_242_a4/

[1] Beklemishev L. D., “Induction rules, reflection principles, and provably recursive functions”, Ann. Pure and Appl. Logic, 85 (1997), 193–242 | DOI | MR | Zbl

[2] Beklemishev L. D., “Open least element principle and bounded query computation”, Computer science logic, Proc. 13th Intern. Workshop CSL'99 (Madrid, Sept. 20–25, 1999), Lect. Notes Comput. Sci., 1683, eds. J. Flum, M. Rodrigues-Artalejo, Springer, Berlin, 1999, 389–404 | MR | Zbl

[3] Beklemishev L. D., “On the schema of induction for decidable predicates”, J. Symb. Logic, 68:1 (2003), 17–34 | DOI | MR | Zbl

[4] Buss S. R., “Introduction to proof theory”, Handbook of proof theory, Elsevier, Amsterdam, 1998, 1–78 | MR | Zbl

[5] Gaifman H., Dimitracopoulos C., “Fragments of Peano's arithmetic and the MDRP theorem”, Logic and algorithmic (Zurich, 1980), Monogr. Enseign. Math., 30, Univ. Genève, Genève, 1982, 187–206 | MR

[6] Hájek P., Pudlák P., Metamathematics of first order arithmetic, Springer, Berlin, Heidelberg, New York, 1993 | MR

[7] Parsons C., “On $n$-quantifier induction”, J. Symb. Logic, 37:3 (1972), 466–482 | DOI | MR | Zbl

[8] Rose H. E., Subrecursion: Functions and hierarchies, Clarendon Press, Oxford, 1984 | MR | Zbl

[9] Sieg W., “Herbrand analyses”, Arch. Math. Logic, 30 (1991), 409–441 | DOI | MR | Zbl

[10] Slaman T. A., “$\Sigma_n$-bounding and $\Delta_n$-induction”, Proc. Amer. Math. Soc (to appear) | MR