Derivatives of normal functions in reverse mathematics
From MaRDI portal
Abstract: Consider a normal function on the ordinals (i. e. a function that is strictly increasing and continuous at limit stages). By enumerating the fixed points of we obtain a faster normal function , called the derivative of . The present paper investigates this important construction from the viewpoint of reverse mathematics. Within this framework we must restrict our attention to normal functions that are represented by dilators (i. e. particularly uniform endofunctors on the category of well-orders, as introduced by J.-Y. Girard). Due to a categorical construction of P. Aczel, each normal dilator has a derivative . We will give a new construction of the derivative, which shows that the existence and fundamental properties of can already be established in the theory . The latter does not prove, however, that preserves well-foundedness. Our main result shows that the statement ``for every normal dilator , its derivative preserves well-foundedness is -provably equivalent to -bar induction (and hence to -dependent choice and to -reflection for -models).
Recommendations
- Normality and exceptional functions of derivatives
- Normality and exceptional values of derivatives
- Differentiation of inverse functions in spaces without norm.
- scientific article; zbMATH DE number 6286530
- On the constants in the inverse theorems for the norms of derivatives
- On norm of functions and their derivatives
- The normal derivative lemma and surrounding issues
- Derivatives of normal functions and \(\omega \)-models
- Normal functions concerning derivatives and shared sets
- Norms and derivatives
Cites work
- \(\Pi_1^1\)-comprehension as a well-ordering principle
- A categorical construction of Bachmann–Howard fixed points
- A note on ordinal exponentiation and derivatives of normal functions
- Computable aspects of the Bachmann-Howard principle
- Derivatives of normal functions and \(\omega \)-models
- Eine Grenze Für die Beweisbarkeit der Transfiniten Induktion in der Verzweigten Typenlogik
- scientific article; zbMATH DE number 3176053 (Why is no real title available?)
- scientific article; zbMATH DE number 3782997 (Why is no real title available?)
- scientific article; zbMATH DE number 3781163 (Why is no real title available?)
- scientific article; zbMATH DE number 3572133 (Why is no real title available?)
- Introduction to \(\Pi^1_2\)-logic
- On the relation between choice and comprehension principles in second order arithmetic
- Proof-theoretic investigations on Kruskal's theorem
- Subsystems of second order arithmetic
- Systems of predicative analysis
- The Veblen functions for computability theorists
- Π12-logic, Part 1: Dilators
Cited in
(14)- Differentiation of inverse functions in spaces without norm.
- Patterns of resemblance and Bachmann-Howard fixed points
- Reflecting and unfolding
- Minimal bad sequences are necessary for a uniform Kruskal theorem
- Calculating Higher Derivatives of Inverses
- Giving reverse differentiation a helping hand∗
- From Kruskal’s theorem to Friedman’s gap condition
- Boundedness theorems for flowers and sharps
- Predicative collapsing principles
- HOW STRONG ARE SINGLE FIXED POINTS OF NORMAL FUNCTIONS?
- WELL ORDERING PRINCIPLES AND -STATEMENTS: A PILOT STUDY
- Well ordering principles for iterated \(\Pi^1_1\)-comprehension
- A note on ordinal exponentiation and derivatives of normal functions
- Induction on dilators and Bachmann-Howard fixed points
This page was built for publication: Derivatives of normal functions in reverse mathematics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2216034)