Recursively saturated and rather classless

A mathematics blog by Kameryn Williams

Category: Paper

Least models of second-order set theories

K. Williams “Least models of second-order set theories” (under review) arXiv PDF bibTeX

Abstract The main theorems of this paper are (1) there is no least transitive model of Kelley–Morse set theory \mathsf{KM} and (2) there is a least \beta-model—that is, a transitive model which is correct about which of its classes are well-founded—of Gödel–Bernays set theory \mathsf{GBC} + Elementary Transfinite Recursion. Along the way I characterize when a countable model of \mathsf{ZFC} has a least \mathsf{GBC}-realization and show that no countable model of \mathsf{ZFC} has a least \mathsf{KM}-realization. I also show that fragments of Elementary Transfinite Recursion have least \beta-models and, for sufficiently weak fragments, least transitive models. These fragments can be separated from each other and from the full principle of Elementary Transfinite Recursion by consistency strength.
The main question left unanswered by this article is whether there is a least transitive model of \mathsf{GBC} + Elementary Transfinite Recursion.

Every set theorist knows there is a least transitive model of \mathsf{ZFC}. What if we want to ask the same question about second-order set theories? Which second-order set theories, if any, have least transitive models? The answer for \mathsf{GBC} follows immediately from the existence of a least transitive model of \mathsf{ZFC}: the least transitive model of \mathsf{GBC} is (L_\alpha, \mathrm{Def}(L_\alpha)) where L_\alpha is the least transitive model of \mathsf{ZFC}. (Indeed, Shepherdson formulated his original argument in terms of \mathsf{GB} (i.e. without Global Choice), rather than in terms of \mathsf{ZFC}.) But this easy argument won’t work for second-order set theories that assert the existence of more classes.

Indeed, no argument will work for sufficiently strong second-order set theories. Take \mathsf{KM}. Allowing for the existence of impredicatively-defined classes means that models of \mathsf{KM} have enough “meta-ordinals” that tools from admissible set theory can be applied. Starting from a model of \mathsf{KM} we can build another model of \mathsf{KM} whose first-order part is the same but whose second-order part sits off to the side, so to speak.

friedman-things

So no (countable) model of \mathsf{ZFC} has a least \mathsf{KM}-realization and thus there cannot be a smallest transitive model of \mathsf{KM}. (Of course, see the actual paper for more than a brief sketch of the argument.)

But \mathsf{KM} is much stronger than \mathsf{GBC} and there are natural theories in the middle. What about those? For \Pi^1_k\text{-}\mathsf{CA} more or less the same argument as the \mathsf{KM} case goes through, getting that they don’t have least transitive models. (But I don’t give a proof of such in this paper; see my forthcoming dissertation for full details.)

So let’s go lower, to the theory \mathsf{ETR}, which is \mathsf{GBC} augmented with the principle of Elementary Transfinite Recursion. Then \mathsf{ETR} is stronger than \mathsf{GBC} because, say, we can construct the Tarskian satisfaction class for first-order formulae via a class recursion of height \omega. But \mathsf{ETR} is strictly weaker than \Pi^1_1\text{-}\mathsf{CA}.

I don’t actually know whether there is a least transitive model of \mathsf{ETR}. (This is the main open question from my paper.) However, I do show that there is a least \beta-model of \mathsf{ETR}. As well, sufficiently weak fragments of \mathsf{ETR}—such as \mathsf{ETR}_{\mathrm{Ord}} which only asserts that elementary transfinite recursions of height \le \mathrm{Ord} have solutions—do have least transitive models. Combined with the results from my joint paper with Gitman, Hamkins, Holy, and Schlict this gives that there is a smallest transitive model of \mathsf{GBC} which satisfies the forcing theorem for all class forcings. I think that’s neat.


Bibtex

@ARTICLE{Williams:least-models,
author = {Kameryn Williams},
title = {Least models of second-order set theories},
journal = {},
year = {},
volume = {},
number = {},
pages = {},
month = {},
note = {manuscript under review},
abstract = {},
keywords = {},
source = {},
doi = {},
eprint = {1709.03955},
archivePrefix = {arXiv},
primaryClass = {math.LO},
url = {https://kamerynblog.wordpress.com/2017/09/12/least-models-of-second-order-set-theories/},
}

Advertisements

The exact strength of the class forcing theorem

V. Gitman, J. D. Hamkins, P. Holy, P. Schlicht, and K. Williams, “The exact strength of the class forcing theorem”. (under review) arXiv bibTeX

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ödel-Bernays set theory \mathsf{GBC} to the principle of elementary transfinite recursion \mathsf{ETR}_{\mathrm{Ord}} for class recursions of length \mathrm{Ord}. It is also equivalent to the existence of truth predicates for the infinitary languages \mathcal{L}_{\mathrm{Ord},\omega}(\in,A), allowing any class parameter A; to the existence of truth predicates for the language \mathcal{L}_{\mathrm{Ord},\mathrm{Ord}}(\in,A); to the existence of \mathrm{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 \mathrm{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 \mathsf{GBC} and Kelley-Morse set theory \mathsf{KM}.

We shall characterize the exact strength of the class forcing theorem, which asserts that every class forcing notion \mathbb{P} has a corresponding forcing relation \Vdash_\mathbb{P}, a relation satisfying the forcing relation recursion. When there is such a forcing relation, then statements true in any corresponding forcing extension are forced and forced statements are true in those extensions.

Unlike set forcing, for which one may prove in \mathsf{ZFC} that every set forcing notion has corresponding forcing relations, with class forcing it is consistent with Gödel-Bernays set theory \mathsf{GBC} that there is a proper class forcing notion lacking a corresponding forcing relation, even merely for the atomic formulas. For certain forcing notions, the existence of an atomic forcing relation implies \mathrm{Con}(\mathsf{ZFC}) and much more, and so the consistency strength of the class forcing theorem strictly exceeds \mathsf{GBC}, if this theory is consistent. Nevertheless, the class forcing theorem is provable in stronger theories, such as Kelley-Morse set theory. What is the exact strength of the class forcing theorem?

Our project here is to identify the strength of the class forcing theorem by situating it in the rich hierarchy of theories between \mathsf{GBC} and \mathsf{KM}. It turns out that the class forcing theorem is equivalent over \mathsf{GBC} to an attractive collection of several other natural set-theoretic assertions; it is a robust axiomatic principle.

ClassForcing.png

The main theorem is naturally part of the emerging subject we call the reverse mathematics of second-order set theory, a higher analogue of the perhaps more familiar reverse mathematics of second-order arithmetic. In this new research area, we are concerned with the hierarchy of second-order set theories between \mathsf{GBC} and \mathsf{KM} and beyond, analyzing the strength of various assertions in second-order set theory, such as the principle \mathsf{ETR} of elementary transfinite recursion, the principle of \Pi^1_1-comprehension or the principle of determinacy for clopen class games. We fit these set-theoretic principles into the hierarchy of theories over the base theory \mathsf{GBC}. The main theorem of this article does exactly this with the class forcing theorem by finding its exact strength in relation to nearby theories in this hierarchy.

Main Theorem

The following are equivalent over Gödel-Bernays set theory.

  1. The atomic class forcing theorem: every class forcing notion admits forcing relations for atomic formulae p\Vdash\sigma=\tau and p\Vdash\sigma\in\tau.
  2. The class forcing theorem schema: for each first-order formula \varphi in the forcing language, with finitely many class names \dot \Gamma_i, there is a forcing relation applicable to this formula and its subformulae p\Vdash\varphi(\vec \tau,\dot\Gamma_0,\ldots,\dot\Gamma_m).
  3. The uniform first-order class forcing theorem: every class forcing notion \mathbb{P} admits a uniform forcing relation p\Vdash\varphi(\vec \tau,\dot\Gamma_0,\ldots,\dot\Gamma_m) applicable to all assertions \varphi\in\mathcal{L}_{\omega,\omega}(\in,V^\mathbb{P},\dot\Gamma_0,\ldots,\dot\Gamma_m) in the first-order forcing language with finitely many class names.
  4. The uniform infinitary class forcing theorem: every class forcing notion \mathbb{P} admits a uniform forcing relation p\Vdash\varphi(\vec \tau,\dot\Gamma_0,\ldots,\dot\Gamma_m) applicable to all assertions \varphi\in\mathcal{L}_{\mathrm{Ord},\mathrm{Ord}}(\in,V^\mathbb{P},\dot\Gamma_0,\ldots,\dot\Gamma_m) in the infinitary forcing language with finitely many class names.
  5. Names for truth predicates: every class forcing notion \mathbb{P} has a class name \dot T and a forcing relation for which \mathbf{1}\Vdash\dot T is a truth-predicate for the first-order forcing language with finitely many class names \mathcal{L}_{\omega,\omega}(\in,V^\mathbb{P},\dot\Gamma_0,\ldots,\dot\Gamma_m).
  6. Boolean completions: Every class forcing notion \mathbb{P}, that is, every separative class partial order, admits a Boolean completion \mathbb B, a set-complete class Boolean algebra into which \mathbb{P} densely embeds.
  7. The class-join separation principle plus \mathsf{ETR}_{\mathrm{Ord}}-foundation.
  8. For every class A, there is a truth predicate for \mathcal{L}_{\mathrm{Ord},\omega}(\in,A).
  9. For every class A, there is a truth predicate for \mathcal{L}_{\mathrm{Ord},\mathrm{Ord}}(\in,A).
  10. For every class A, there is an \mathrm{Ord}-iterated truth predicate for \mathcal{L}_{\omega,\omega}(\in,A).
  11. The principle of determinacy for clopen class games of rank at most \mathrm{Ord}+1.
  12. The principle \mathsf{ETR}_{\mathrm{Ord}} of elementary transfinite recursion for \mathrm{Ord}-length recursions of first-order properties, using any class parameter.

Bibtex

@ARTICLE{GitmanHamkinsHolySchlichtWilliams:The-exact-strength-of-the-class-forcing-theorem,
author = {Victoria Gitman and Joel David Hamkins and Peter Holy and Philipp Schlicht and Kameryn Williams},
title = {The exact strength of the class forcing theorem},
journal = {},
year = {},
volume = {},
number = {},
pages = {},
month = {},
note = {manuscript under review},
abstract = {},
keywords = {},
source = {},
doi = {},
eprint = {1707.03700},
archivePrefix = {arXiv},
primaryClass = {math.LO},
url = {http://jdh.hamkins.org/class-forcing-theorem},
}