{
  "id": "1904.04630",
  "version": "v1",
  "published": "2019-04-09T12:51:25.000Z",
  "updated": "2019-04-09T12:51:25.000Z",
  "title": "Derivatives of normal functions in reverse mathematics",
  "authors": [
    "Anton Freund",
    "Michael Rathjen"
  ],
  "categories": [
    "math.LO"
  ],
  "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'$, 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:\\aleph_1\\rightarrow\\aleph_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 $\\partial T$. We will give a new construction of the derivative, which shows that the existence and fundamental properties of $\\partial T$ can already be established in the theory $\\mathbf{RCA_0}$. The latter does not prove, however, that $\\partial T$ preserves well-foundedness. Our main result shows that the statement `for every normal dilator $T$, its derivative $\\partial T$ preserves well-foundedness' is $\\mathbf{ACA_0}$-provably equivalent to $\\Pi^1_1$-bar induction (and hence to $\\Sigma^1_1$-dependent choice and to $\\Pi^1_2$-reflection for $\\omega$-models).",
  "revisions": [
    {
      "version": "v1",
      "updated": "2019-04-09T12:51:25.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "03F15",
      "03F35",
      "03D60",
      "03E10"
    ],
    "keywords": [
      "reverse mathematics",
      "derivative",
      "preserves well-foundedness",
      "normal dilator",
      "faster normal function"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 0,
      "language": "en",
      "license": "arXiv",
      "status": "editable"
    }
  }
}