Universes over Frege structures
type: Item
instance of: scholarly article
title: Universes over Frege structures
zbMATH Open document ID: 1018.03046
DOI: 10.1016/S0168-0072(02)00040-4
author: Reinhard Kahle
published in: Annals of Pure and Applied Logic
publication date: 2003-03-09T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03F25
Mathematics Subject Classification ID: 03F35
zbMATH DE Number: 1878505
zbMATH Keywords: proof-theoretic strength
zbMATH Keywords: Frege structures with universes
zbMATH Keywords: inductive definitions
MaRDI profile type: Publication
cites work: Q3912779
cites work: Q4075450
cites work: Q3679172
cites work: Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
cites work: Q3705449
cites work: On the relation between choice and comprehension principles in second order arithmetic
cites work: Notes on Formal Theories of Truth
cites work: A theory of formal truth arithmetically equivalent to ID1
cites work: Extending the first-order theory of combinators with self-referential truth
cites work: Levels of truth
cites work: Logical frameworks for truth and abstraction. An axiomatic study
cites work: Q4128540
cites work: Q3882452
cites work: Q3671968
cites work: Hilbert's program relativized; Proof-theoretical and foundational reductions
cites work: Does reductive proof theory have a viable rationale?
cites work: Systems of explicit mathematics with non-constructive \(\mu\)-operator. I
cites work: Systems of explicit mathematics with non-constructive \(\mu\)-operator. II
cites work: The unfolding of non-finitist arithmetic
cites work: Q3812243
cites work: Implication and analysis in classical Frege structures
cites work: Q4302420
cites work: Understanding uniformity in Feferman's explicit mathematics
cites work: Systems of explicit mathematics with non-constructive \(\mu\)-operator and join
cites work: A NEW FORMALIZATION OF FEFERMAN’S SYSTEM OF FUNCTIONS AND CLASSES AND ITS RELATION TO FREGE STRUCTURE
cites work: Q4146722
cites work: Beweistheorie vonKPN
cites work: The strength of admissibility without foundation
cites work: Fixed points in Peano arithmetic with ordinals
cites work: The proof-theoretic analysis of transfinitely iterated fixed point theories
cites work: Q4941991
cites work: Universes in explicit mathematics
cites work: Second order theories with ordinals and elementary comprehension
cites work: Totality in applicative theories
cites work: Some theories with positive induction of ordinal strength φω0
cites work: Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory
cites work: Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms
cites work: Frege structures for partial applicative theories
cites work: Truth in applicative theories
cites work: Q4283245
cites work: The \(\mu\) quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals
cites work: Q3773877
cites work: The strength of Martin-Löf type theory with a superuniverse. I
cites work: The strength of Martin-Löf type theory with a superuniverse. II
cites work: Universes in metapredicative analysis
cites work: Q4143279
cites work: Q4934566
cites work: Q4220572
cites work: Partial Applicative Theories and Explicit Substitutions
cites work: Q4934569
cites work: Q4944925
cites work: The non-constructive \(\mu\) operator, fixed point theories with ordinals, and the bar rule
cites work: Q5605873
description: scientific article; zbMATH DE number 1878505