×

zbMATH — the first resource for mathematics

Universes over Frege structures. (English) Zbl 1018.03046
The author determines the proof-theoretic strengths of FSU (the theory of Frege structures with universes) with three forms of (mathematical) induction. FSU itself is built on an applicative theory with the truth predicate \(T(\cdot)\), and inductions are labelled C-In (class induction), T-In (truth), and F-In (formula). The last, F-In, begins with \(\varphi(0) \wedge \dots\) for any formula \(\varphi\), T-In with \(T(f0)\wedge\dots\) where \(f\) is a variable, and C-In has an additional formula ‘if \(f\) is a class’ before \(T(f0) \wedge\dots\). The strengths of FSU+C-In, of FSU+T-In and of FSU+F-In are shown to be the same as those of the theories of inductive definitions \(\widehat {\text{ID}}_{<\omega}\), \(\widehat{\text{ID}}_{<\omega^\omega}\), and \(\widehat {\text{ID}}_{<\varepsilon_0}\), respectively. The proof goes in two ways, of course. The author gives a translation of the ID-language into the FSU-language. In the other direction, the FSU systems are put into an infinitary system, and term models are handled in relevant ID theories.
The author gives not just technical accounts, but writes in a wider context, beginning with Frege structures, and including recent activities at Bern, and other results.

MSC:
03F25 Relative consistency and interpretations
03F35 Second- and higher-order arithmetic and fragments
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] P. Aczel, The strength of Martin Löf’s intuitionistic type theory with one universe, in: S. Miettinen, J. Väänänen (Eds.), Proceedings of the Symposiums on Mathematical Logic in Oulo 1974 and in Helsinki 1975, Report No. 2, Department of Philosophy, University of Helsinki, 1977.
[2] Aczel, P., Frege structures and the notion of proposition, truth and set, (), 31-59
[3] Barwise, J., Admissible sets and structures, (1975), Springer Berlin · Zbl 0316.02047
[4] M. Beeson, Foundations of Constructive Mathematics, Ergebnisse der Mathematik und ihrer Grenzgebiete; 3.Folge, Bd. 6, Springer, Berlin, 1985.
[5] Buchholz, W.; Feferman, S.; Pohlers W. Sieg, W., Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies, Lecture notes in mathematics, Vol. 897, (1981), Springer Berlin · Zbl 0489.03022
[6] A. Cantini, A note on a predicatively reducible theory of iterated elementary induction, Bull. Unione Math. Italiana, Serie VI, IV-B (2) (1985) 413-430. · Zbl 0582.03043
[7] Cantini, A., On the relationship between choice and comprehension principles in second order arithmetic, J. symbolic logic, 51, 360-373, (1986) · Zbl 0632.03046
[8] Cantini, A., Notes on formal theories of truth, Z. math. logik grundlag. math., 35, 97-130, (1989) · Zbl 0661.03043
[9] Cantini, A., A theory of formal truth arithmetically equivalent to \(ID1\), J. symbolic logic, 55, 1, 244-259, (1990) · Zbl 0713.03029
[10] Cantini, A., Extending the first-order theory of combinators with self-referential truth, J. symbolic logic, 58, 2, 477-513, (1993) · Zbl 0795.03075
[11] Cantini, A., Levels of truth, Notre dame J. formal logic, 36, 185-213, (1995) · Zbl 0836.03033
[12] Cantini, A., Logical frameworks for truth and abstraction, (1996), North-Holland Amsterdam · Zbl 0860.03015
[13] Feferman, S., A language and axioms for explicit mathematics, (), 87-139
[14] Feferman, S., Constructive theories of functions and classes, (), 159-224
[15] Feferman, S., Iterated inductive fixed-point theoriesapplication to Hancock’s conjecture, (), 171-196
[16] Feferman, S., Hilbert’s program relativizedproof-theoretical and foundational reductions, J. symbolic logic, 53, 2, 364-384, (1988) · Zbl 0656.03002
[17] Feferman, S., Does reductive proof theory have a viable rationale?, Erkenntnis, 53, 1-2, 63-96, (2000) · Zbl 0971.03058
[18] Feferman, S.; Jäger, G., Systems of explicit mathematics with non-constructive μ-operator. part I, Ann. pure appl. logic, 65, 3, 243-263, (1993) · Zbl 0794.03074
[19] Feferman, S.; Jäger, G., Systems of explicit mathematics with non-constructive μ-operator. part II, Ann. pure appl. logic, 79, 37-52, (1996) · Zbl 0868.03026
[20] Feferman, S.; Strahm, T., The unfolding of non-finitist arithmetic, Ann. pure appl. logic, 104, 1-3, 75-96, (2000) · Zbl 0959.03048
[21] Flagg, R.; Myhill, J., An extension of frege structures, (), 197-217
[22] Flagg, R.; Myhill, J., Implication and analysis in classical frege structures, Ann. pure appl. logic, 34, 33-85, (1987) · Zbl 0632.03045
[23] T. Glaß, Standardstrukturen für Systeme Expliziter Mathematik, Ph.D. Thesis, Westfälische Wilhelms-Universität Münster, 1993.
[24] Glaß, T., Understanding uniformity in Feferman’s explicit mathematics, Ann. pure appl. logic, 75, 1-2, 89-106, (1995) · Zbl 0845.03026
[25] Glaß, T.; Strahm, T., Systems of explicit mathematics with non-constructive μ-operator and join, Ann. pure appl. logic, 82, 2, 193-219, (1996) · Zbl 0862.03028
[26] Hayashi, S.; Kobayashi, S., A new formulation of Feferman’s system of functions and classes and its relation to frege structures, Internat. J. found. comput. sci., 6, 3, 187-202, (1995) · Zbl 0830.68114
[27] Hinman, P., Recursion-theoretic hierarchies, (1978), Springer Berlin · Zbl 0371.02017
[28] Jäger, G., Beweistheorie von KPN, Arch. math. logik grundlag., 20, 53-64, (1980)
[29] Jäger, G., The strength of admissibility without foundation, J. symbolic logic, 49, 3, 867-879, (1984) · Zbl 0585.03032
[30] Jäger, G., Fixed points in Peano arithmetic with ordinals, Ann. pure appl. logic, 60, 119-132, (1993) · Zbl 0776.03027
[31] G. Jäger, Metapredicative and explicit Mahlo: a proof-theoretic perspective, in: Logic Colloquium 2000, Lecture Note in Logic, ed., A.K. Peters, Natick, 200x, to appear.
[32] Jäger, G.; Kahle, R.; Setzer, A.; Strahm, T., The proof-theoretic analysis of transfinitely iterated fixed point theories, J. symbolic logic, 64, 1, 53-67, (1999) · Zbl 0937.03065
[33] Jäger, G.; Kahle, R.; Strahm, T., On applicative theories, (), 88-92 · Zbl 0951.03054
[34] Jäger, G.; Kahle, R.; Studer, T., Universes in explicit mathematics, Ann. pure appl. logic, 109, 3, 141-162, (2001) · Zbl 0980.03061
[35] Jäger, G.; Strahm, T., Second order theories with ordinals and elementary comprehension, Arch. math. logic, 34, 6, 345-375, (1995) · Zbl 0846.03028
[36] Jäger, G.; Strahm, T., Totality in applicative theories, Ann. pure appl. logic, 74, 105-120, (1995) · Zbl 0832.03027
[37] Jäger, G.; Strahm, T., Some theories with positive induction of ordinal strength ϕω 0, J. symbolic logic, 61, 3, 818-842, (1996) · Zbl 0862.03031
[38] Jäger, G.; Strahm, T., Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory, J. symbolic logic, 66, 2, 935-958, (2001) · Zbl 1011.03046
[39] Jäger, G.; Studer, T., Extending the system \(T0\) of explicit mathematics: the limit and Mahlo axioms, Ann. pure appl. logic, 114, 79-101, (2002) · Zbl 1002.03052
[40] R. Kahle, Applikative Theorien und Frege-Strukturen, Ph.D. Thesis, Institut für Informatik und angewandte Mathematik, Universität Bern, 1997.
[41] R. Kahle, Uniform limit in explicit mathematics with universes, Technical Report IAM-97-002, IAM, Universität Bern, 1997.
[42] Kahle, R., Frege structures for partial applicative theories, J. logic comput., 9, 5, 683-700, (1999) · Zbl 0941.03065
[43] Kahle, R., Truth in applicative theories, Stud. logica, 68, 1, 103-128, (2001) · Zbl 0988.03083
[44] Martin-Löf, P., Intuitionistic type theory, (1984), Bibliopolis Napoli
[45] Marzetta, M., Universes in the theory of types and names, (), 340-351 · Zbl 0794.03083
[46] M. Marzetta, Predicative theories of types and names, Ph.D. Thesis, Universtiät Bern, Institut für Informatik und angewandte Mathematik, 1994.
[47] Marzetta, M.; Strahm, T., The μ quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals, Arch. math. logic, 37, 5-6, 391-413, (1998) · Zbl 0920.03057
[48] Pohlers, W., Proof theory, Lecture notes in mathematics, Vol. 1407, (1989), Springer Berlin · Zbl 0635.03053
[49] Rathjen, M., The strength of martin-Löf type theory with a superuniverse. part I, Arch. math. logic, 39, 1, 1-39, (2000) · Zbl 0953.03065
[50] Rathjen, M., The strength of martin-Löf type theory with a superuniverse. part II, Arch. math. logic, 40, 3, 207-233, (2001) · Zbl 0990.03048
[51] C. Rüede, Metapredicative subsystems of analysis, Ph.D. Thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2000.
[52] C. Rüede, Dependent choice and ω model reflection, J. Symbolic Logic, 200x, to appear.
[53] C. Rüede, Universes in metapredicative analysis, Arch. Math. Logic, 200x, to appear. · Zbl 1031.03073
[54] Schütte, K., Proof theory, Grundlehren der mathematischen wissenschaften, Vol. 225, (1977), Springer Berlin
[55] Scott, D., Combinators and classes, (), 1-26
[56] Setzer, A., Ordinal systems, (), 301-338 · Zbl 0944.03054
[57] Simpson, S., Subsystems of second order arithmetic, perspectives in mathematical logic, (1999), Springer Berlin
[58] T. Strahm, On the proof theory of applicative theories, Ph.D. Thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 1996. · Zbl 0841.03005
[59] Strahm, T., First steps into metapredicativity in explicit mathematics, (), 383-402 · Zbl 0961.03057
[60] Strahm, T., Autonomous fixed point progressions and fixed point transfinite recursion, (), 449-464 · Zbl 0943.03044
[61] Strahm, T., The non-constructive μ-operator, fixed point theories with ordinals, and the bar rule, Ann. pure appl. logic, 104, 1-3, 305-324, (2000) · Zbl 0964.03061
[62] Tait, W., Normal derivability in classical logic, (), 204-236 · Zbl 0206.00502
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.