{
  "id": "1312.1531",
  "version": "v2",
  "published": "2013-12-05T13:08:12.000Z",
  "updated": "2015-04-08T05:49:35.000Z",
  "title": "Measure theory and higher order arithmetic",
  "authors": [
    "Alexander P. Kreuzer"
  ],
  "categories": [
    "math.LO"
  ],
  "abstract": "We investigate the statement that the Lebesgue measure defined on all subsets of the Cantor space exists. As base system we take $\\mathsf{ACA}_0^\\omega + (\\mu)$. The system $\\mathsf{ACA}_0^\\omega$ is the higher order extension of Friedman's system $\\mathsf{ACA}_0$, and $(\\mu)$ denotes Feferman's $\\mu$, that is a uniform functional for arithmetical comprehension defined by $f(\\mu(f))=0$ if $\\exists n f(n)=0$ for $f\\in \\mathbb{N}^\\mathbb{N}$. Feferman's $\\mu$ will provide countable unions and intersections of sets of reals and is, in fact, equivalent to this. For this reasons $\\mathsf{ACA}_0^\\omega + (\\mu)$ is the weakest fragment of higher order arithmetic where $\\sigma$-additive measures are directly definable. We obtain that over $\\mathsf{ACA}_0^\\omega + (\\mu)$ the existence of the Lebesgue measure is $\\Pi^1_2$-conservative over $\\mathsf{ACA}_0^\\omega$ and with this conservative over $\\mathsf{PA}$. Moreover, we establish a corresponding program extraction result.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2013-12-05T13:08:12.000Z",
      "comment": null,
      "journal": null,
      "doi": null
    },
    {
      "version": "v2",
      "updated": "2015-04-08T05:49:35.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "03F35",
      "03B30",
      "03E35"
    ],
    "keywords": [
      "higher order arithmetic",
      "measure theory",
      "lebesgue measure",
      "corresponding program extraction result",
      "higher order extension"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 0,
      "language": "en",
      "license": "arXiv",
      "status": "editable",
      "adsabs": "2013arXiv1312.1531K"
    }
  }
}