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

bar inductionderivativesdilatorsnormal functions (on the ordinals)ordinal notationsreverse mathematicswell-ordering principles

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) Recursive ordinals and ordinal notations (03F15) Second- and higher-order arithmetic and fragments (03F35)

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).

Review text

It is well known that continuous, strictly increasing -- or ``normal -- class functions on ordinals are in direct correspondence with closed and unbounded (club) classes of ordinals. The fixed point set of such a function is a club, and thus it is described by another such function, called the \textit{derivative} of the original one. In this paper, this normal function property of having a derivative is studied reverse-mathematically. To do that, normal functions are restricted first to (ordinary set-theoretic) functions defined on \(\aleph_1\) (making use of its regularity) and then to those which are describable by dilators (for which the derivative may be described in a more elegant way). Thus, in this restricted sense, the property is shown to be equivalent over \(\textbf{ACA}_0\) (this was later weakened to \(\textbf{RCA}_0\) in a separate paper of Anton Freund, the first author of this paper) to the principle of \(\Pi^1_1\)-bar induction (also called transfinite induction).

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)