Derivatives of normal functions in reverse mathematics

DOI10.1016/J.APAL.2020.102890MaRDI QIDQ2216034zbMATH OpenOpenAlexFDO

Authors Anton Freund, Michael Rathjen

Publication date 15 December 2020

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1904.04630

zbMATH Keywords

reverse mathematicsderivativesbar inductionordinal notationswell-ordering principlesdilatorsnormal functions (on the ordinals)

Mathematics Subject Classification ID

Foundations of classical theories (including reverse mathematics) (03B30) Computability and recursion theory on ordinals, admissible sets, etc. (03D60) Ordinal and cardinal numbers (03E10) Second- and higher-order arithmetic and fragments (03F35) Recursive ordinals and ordinal notations (03F15)

Abstract: Consider a normal function $f$ on the ordinals (i. e. a function $f$ that is strictly increasing and continuous at limit stages). By enumerating the fixed points of $f$ we obtain a faster normal function $f^{\prime }$, called the derivative of $f$. The present paper investigates this important construction from the viewpoint of reverse mathematics. Within this framework we must restrict our attention to normal functions $f:alep{h}_{1}ightarrowalep{h}_1$ 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 $T$ has a derivative $partialT$. We will give a new construction of the derivative, which shows that the existence and fundamental properties of $partialT$ can already be established in the theory $mathbf{RCA}_0$. The latter does not prove, however, that $partialT$ preserves well-foundedness. Our main result shows that the statement ``for every normal dilator $T$, its derivative $partialT$ preserves well-foundedness is $mathbf{ACA}_0$-provably equivalent to $P{i}_1^1$-bar induction (and hence to $Sigm{a}_1^1$-dependent choice and to $P{i}_2^1$-reflection for $omega$-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

• 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?)
• 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
• 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
• \(\Pi_1^1\)-comprehension as a well-ordering principle
• Π12-logic, Part 1: Dilators

Cited in

(13)

• Boundedness theorems for flowers and sharps
• WELL ORDERING PRINCIPLES AND -STATEMENTS: A PILOT STUDY
• Predicative collapsing principles
• Minimal bad sequences are necessary for a uniform Kruskal theorem
• HOW STRONG ARE SINGLE FIXED POINTS OF NORMAL FUNCTIONS?
• A note on ordinal exponentiation and derivatives of normal functions
• From Kruskal’s theorem to Friedman’s gap condition
• Giving reverse differentiation a helping hand^∗
• Well ordering principles for iterated \(\Pi^1_1\)-comprehension
• Calculating Higher Derivatives of Inverses
• Patterns of resemblance and Bachmann-Howard fixed points
• Differentiation of inverse functions in spaces without norm.
• Reflecting and unfolding

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)