On elementary theories of ordinal notation systems based on reflection principles

F. N. Pakhomov

Informatics and Automation, Selected issues of mathematics and mechanics, Tome 289 (2015), pp. 206-226.

Résumé

L.D. Beklemishev has recently introduced a constructive ordinal notation system for the ordinal $\varepsilon _0$. We consider this system and its fragments for smaller ordinals $\omega _n$ (towers of $\omega $-exponentiations of height $n$). These systems are based on Japaridze's well-known polymodal provability logic. They are used in the technique of ordinal analysis of the Peano arithmetic $\mathbf {PA}$ and its fragments on the basis of iterated reflection schemes. Ordinal notation systems can be regarded as models of the first-order language. We prove that the full notation system and its fragments for ordinals ${\ge }\,\omega _4$ have undecidable elementary theories. At the same time, the fragments of the full system for ordinals ${\le }\,\omega _3$ have decidable elementary theories. We also obtain results on decidability of the elementary theory for ordinal notation systems with weaker signatures.

Bibliographie

[1] Beklemishev L. D., “Proof-theoretic analysis by iterated reflection”, Arch. Math. Logic, 42:6 (2003), 515–552 | DOI | MR | Zbl

[2] Beklemishev L. D., “Provability algebras and proof-theoretic ordinals. I”, Ann. Pure Appl. Logic, 128 (2004), 103–123 | DOI | MR | Zbl

[3] Beklemishev L. D., “Veblen hierarchy in the context of provability algebras”, Logic, methodology and philosophy of science, Proc. 12th Int. Congr. (Oviedo, Spain, 2003), King's College Publ., London, 2005, 65–78 | Zbl

[4] Beklemishev L. D., “Skhemy refleksii i algebry dokazuemosti v formalnoi arifmetike”, UMN, 60:2 (2005), 3–78 | DOI | MR | Zbl

[5] Braud L., “Covering of ordinals”, IARCS Annu. Conf. on Foundations of Software Technology and Theoretical Computer Science (Kanpur, India, 2009), Leibniz Int. Proc. Inf., 4, Schloss Dagstuhl–Leibniz Zentrum Inf., Wadern, 2009, 97–108 | MR | Zbl

[6] Büchi J. R., “Decision methods in the theory of ordinals”, Bull. Amer. Math. Soc., 71 (1965), 767–770 | DOI | MR | Zbl

[7] Carlucci L., “Worms, gaps, and hydras”, Math. Logic Q., 51:4 (2005), 342–350 | DOI | MR | Zbl

[8] Church A., “The constructive second number class”, Bull. Amer. Math. Soc., 44 (1938), 224–232 | DOI | MR | Zbl

[9] Doner J. E., Mostowski A., Tarski A., “The elementary theory of well-ordering – a metamathematical study”, Proc. Logic Colloquium'77, Stud. Logic Found. Math., 96, North-Holland, Amsterdam, 1978, 1–54 | MR

[10] Ehrenfeucht A., “An application of games to the completeness problem for formalized theories”, Fundam. math., 49 (1961), 129–141 | MR | Zbl

[11] Gentzen G., “Die Widerspruchsfreiheit der reinen Zahlentheorie”, Math. Ann., 112 (1936), 493–565 | DOI | MR | Zbl

[12] Hájek P., Pudlák P., Metamathematics of first-order arithmetic, Springer, Berlin, 1998 | MR | Zbl

[13] Ignatiev K. N., “On strong provability predicates and the associated modal logics”, J. Symb. Logic, 58:1 (1993), 249–290 | DOI | MR | Zbl

[14] Dzhaparidze G. K., Modalno-logicheskie sredstva issledovaniya dokazuemosti, Dis. $\dots$ kand. filos. nauk, MGU, M., 1986

[15] Kleene S. C., “On notation for ordinal numbers”, J. Symb. Logic, 3:4 (1938), 150–155 | DOI | MR | Zbl

[16] Kreisel G., “Wie die Beweistheorie zu ihren Ordinalzahlen kam und kommt”, Jahresber. Dtsch. Math.-Ver., 78:4 (1977), 177–223 ; Kraizel G., “Kak teoriya dokazatelstv prishla k svoim ordinalnym chislam i kak ona prikhodit k nim teper”, Issledovaniya po teorii dokazatelstv, Matematika. Novoe v zarubezhnoi nauke, 23, Mir, M., 1981, 183–238 | MR | Zbl

[17] Lavrov I. A., “Effektivnaya neotdelimost mnozhestva tozhdestvenno istinnykh i mnozhestva konechno oproverzhimykh formul nekotorykh teorii”, Algebra i logika, 2:1 (1963), 5–18 | MR | Zbl

[18] Lee G., “A comparison of well-known ordinal notation systems for $\varepsilon_0$”, Ann. Pure Appl. Logic, 147 (2007), 48–70 | DOI | MR | Zbl

[19] Mostowski A., Tarski A., “Arithmetical classes and types of well ordered systems”, Bull. Amer. Math. Soc., 55:1 (1949), 65 | MR

[20] Pakhomov F. N., “Nerazreshimost elementarnoi teorii polureshetki $\mathrm{GLP}$-slov”, Mat. sb., 203:8 (2012), 141–160 | DOI | MR | Zbl

[21] Pohlers W., Proof theory: The first step into impredicativity, Universitext, Springer, Berlin, 2008 | MR

[22] Rathjen M., “The realm of ordinal analysis”, Sets and proofs, LMS Lect. Note Ser., 258, Cambridge Univ. Press, Cambridge, 1999, 219–279 | MR | Zbl

[23] Rogers H. (Jr.), Theory of recursive functions and effective computability, MIT Press, Cambridge, MA, 1987 | MR

[24] Schütte K., Simpson S. G., “Ein in der reinen Zahlentheorie unbeweisbarer Satz über endliche Folgen von natürlichen Zahlen”, Arch. Math. Logik Grundlagenforsch., 25 (1985), 75–89 | DOI | MR | Zbl

[25] Takeuti G., Teoriya dokazatelstv, Mir, M., 1978 | MR