{
  "id": "1707.03700",
  "version": "v1",
  "published": "2017-07-12T13:21:08.000Z",
  "updated": "2017-07-12T13:21:08.000Z",
  "title": "The exact strength of the class forcing theorem",
  "authors": [
    "Victoria Gitman",
    "Joel David Hamkins",
    "Peter Holy",
    "Philipp Schlicht",
    "Kameryn Williams"
  ],
  "comment": "34 pages. Commentary concerning this paper can be made at http://jdh.hamkins.org/class-forcing-theorem",
  "categories": [
    "math.LO"
  ],
  "abstract": "The class forcing theorem, which asserts that every class forcing notion $\\mathbb{P}$ admits a forcing relation $\\Vdash_{\\mathbb{P}}$, that is, a relation satisfying the forcing relation recursion---it follows that statements true in the corresponding forcing extensions are forced and forced statements are true---is equivalent over G\\\"odel-Bernays set theory GBC to the principle of elementary transfinite recursion $\\text{ETR}_{\\text{Ord}}$ for class recursions of length $\\text{Ord}$. It is also equivalent to the existence of truth predicates for the infinitary languages $\\mathcal{L}_{\\text{Ord},\\omega}(\\in,A)$, allowing any class parameter $A$; to the existence of truth predicates for the language $\\mathcal{L}_{\\text{Ord},\\text{Ord}}(\\in,A)$; to the existence of $\\text{Ord}$-iterated truth predicates for first-order set theory $\\mathcal{L}_{\\omega,\\omega}(\\in,A)$; to the assertion that every separative class partial order $\\mathbb{P}$ has a set-complete class Boolean completion; to a class-join separation principle; and to the principle of determinacy for clopen class games of rank at most $\\text{Ord}+1$. Unlike set forcing, if every class forcing notion $\\mathbb{P}$ has a forcing relation merely for atomic formulas, then every such $\\mathbb{P}$ has a uniform forcing relation applicable simultaneously to all formulas. Our results situate the class forcing theorem in the rich hierarchy of theories between GBC and Kelley-Morse set theory KM.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2017-07-12T13:21:08.000Z"
    }
  ],
  "analyses": {
    "keywords": [
      "class forcing theorem",
      "forcing relation",
      "exact strength",
      "truth predicates",
      "class forcing notion"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 34,
      "language": "en",
      "license": "arXiv",
      "status": "editable"
    }
  }
}