Kameryn J. Williams, PhD 2018, CUNY Graduate Center

Kameryn J. Williams successfully defended his dissertation under my supervision at the CUNY Graduate Center on April 6th, 2018, earning his Ph.D. degree in May 2018. He has accepted a position in mathematics at the University of Hawaii, to begin Fall 2018.

What a pleasure it was to work with Kameryn, an extremely talented mathematician with wide interests and huge promise.

Recursively saturated and rather classlessMathOverflow | ar$\chi$iv

Kameryn J. Williams, The Structure of Models of Second-order Set Theories,  Ph.D. dissertation for The Graduate Center of the City University of New York, May, 2018. arXiv:1804.09526.

Abstract. This dissertation is a contribution to the project of second-order set theory, which has seen a revival in recent years. The approach is to understand second-order set theory by studying the structure of models of second-order set theories. The main results are the following, organized by chapter. First, I investigate the poset of T-realizations of a fixed countable model of ZFC, where T is a reasonable second-order set theory such as GBC or KM, showing that it has a rich structure. In particular, every countable partial order embeds into this structure. Moreover, we can arrange so that these embedding preserve the existence/nonexistence of upper bounds, at least for finite partial orders. Second I generalize some constructions of Marek and Mostowski from KM to weaker theories. They showed that every model of KM plus the Class Collection schema “unrolls” to a model of ZFC− with a largest cardinal. I calculate the theories of the unrolling for a variety of second-order set theories, going as weak as GBC + ETR. I also show that being T-realizable goes down to submodels for a broad selection of second-order set theories T. Third, I show that there is a hierarchy of transfinite recursion principles ranging in strength from GBC to KM. This hierarchy is ordered first by the complexity of the properties allowed in the recursions and second by the allowed heights of the recurions. Fourth, I investigate the question of which second-order set theories have least models. I show that strong theories—such as KM or $\Pi^1_1$-CA—do not have least transitive models, while weaker theories—from GBC to GBC + ETR${}_{\text{Ord}}$—do have least transitive models.

In addition to his dissertation work and the research currently arising out of it, Kameryn has undertaken a number of collaborations with various international research efforts, including the following:

  • He is a co-author on 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,” ArXiv e-prints, 2017. (manuscript under review)  
      @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 = {ArXiv e-prints},
      year = {2017},
      month = {July},
      volume = {},
      number = {},
      pages = {},
      note = {manuscript under review},
      abstract = {},
      keywords = {under-review},
      source = {},
      doi = {},
      eprint = {1707.03700},
      archivePrefix = {arXiv},
      primaryClass = {math.LO},
      url = {http://jdh.hamkins.org/class-forcing-theorem},
      }

  • He is co-author on a current joint project with Miha Habič, myself, Daniel Klausner and Jonathan Verner concerning the nonamalgamation phenomenon in the generic multiverse of a countable model of set theory.
  • He is co-author on a current joint project with myself and Philip Welch concerning the universal $\Sigma_1$-definable finite sequence, an analogue of the universal finite set, but for the constructible universe.

 

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,” ArXiv e-prints, 2017. (manuscript under review)  
    @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 = {ArXiv e-prints},
    year = {2017},
    month = {July},
    volume = {},
    number = {},
    pages = {},
    note = {manuscript under review},
    abstract = {},
    keywords = {under-review},
    source = {},
    doi = {},
    eprint = {1707.03700},
    archivePrefix = {arXiv},
    primaryClass = {math.LO},
    url = {http://jdh.hamkins.org/class-forcing-theorem},
    }

Abstract. The class forcing theorem, which asserts that every class forcing notion $\newcommand\P{\mathbb{P}}\P$ admits a forcing relation $\newcommand\forces{\Vdash}\forces_\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 GBC to the principle of elementary transfinite recursion $\newcommand\Ord{\text{Ord}}\newcommand\ETR{\text{ETR}}\ETR_{\Ord}$ for class recursions of length $\Ord$. It is also equivalent to the existence of truth predicates for the infinitary languages $\mathcal{L}_{\Ord,\omega}(\in,A)$, allowing any class parameter $A$; to the existence of truth predicates for the language $\mathcal{L}_{\Ord,\Ord}(\in,A)$; to the existence of $\Ord$-iterated truth predicates for first-order set theory $\mathcal{L}_{\omega,\omega}(\in,A)$; to the assertion that every separative class partial order $\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 $\Ord+1$. Unlike set forcing, if every class forcing relation $\P$ has a forcing relation merely for atomic formulas, then every such $\P$ has a uniform forcing relation that applies uniformly to all formulas. Our results situate the class forcing theorem in the rich hierarchy of theories between GBC and Kelley-Morse set theory KM.

We shall characterize the exact strength of the class forcing theorem, which asserts that every class forcing notion $\P$ has a corresponding forcing relation $\forces_\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 the case of set forcing, where one may prove in ZFC that every set forcing notion has corresponding forcing relations, for class forcing it is consistent with Gödel-Bernays set theory 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 Con(ZFC) and much more, and so the consistency strength of the class forcing theorem strictly exceeds 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 GBC and KM, displayed in part in the figure above, with the class forcing theorem highlighted in blue. It turns out that the class forcing theorem is equivalent over GBC to an attractive collection of several other natural set-theoretic assertions; it is a robust axiomatic principle.

Hierarchy between GBC and KM

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 GBC and KM and beyond, analyzing the strength of various assertions in second-order set theory, such as the principle 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 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 formulas $$p\forces\sigma=\tau\qquad\qquad p\forces\sigma\in\tau.$$
  2. The class forcing theorem scheme: 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 subformulas
    $$p\forces\varphi(\vec \tau,\dot\Gamma_0,\ldots,\dot\Gamma_m).$$
  3. The uniform first-order class forcing theorem: every class forcing notion $\P$ admits a uniform forcing relation $$p\forces\varphi(\vec \tau),$$ applicable to all assertions $\varphi$ in the first-order forcing language with finitely many class names $\mathcal{L}_{\omega,\omega}(\in,V^\P,\dot\Gamma_0,\ldots,\dot\Gamma_m)$.
  4. The uniform infinitary class forcing theorem: every class forcing notion $\P$ admits a uniform forcing relation $$p\forces\varphi(\vec \tau),$$ applicable to all assertions $\varphi$ in the infinitary forcing language with finitely many class names $\mathcal{L}_{\Ord,\Ord}(\in,V^\P,\dot\Gamma_0,\ldots,\dot\Gamma_m)$.
  5. Names for truth predicates: every class forcing notion $\P$ has a class name $\newcommand\T{{\rm T}}\dot\T$ and a forcing relation for which $1\forces\dot\T$ is a truth-predicate for the first-order forcing language with finitely many class names $\mathcal{L}_{\omega,\omega}(\in,V^\P,\dot\Gamma_0,\ldots,\dot\Gamma_m)$.
  6. Every class forcing notion $\P$, that is, every separative class partial order, admits a Boolean completion $\mathbb{B}$, a set-complete class Boolean algebra into which $\P$ densely embeds.
  7. The class-join separation principle plus $\ETR_{\Ord}$-foundation.
  8. For every class $A$, there is a truth predicate for $\mathcal{L}_{\Ord,\omega}(\in,A)$.
  9. For every class $A$, there is a truth predicate for $\mathcal{L}_{\Ord,\Ord}(\in,A)$.
  10. For every class $A$, there is an $\Ord$-iterated truth predicate for $\mathcal{L}_{\omega,\omega}(\in,A)$.
  11. The principle of determinacy for clopen class games of rank at most $\Ord+1$.
  12. The principle $\ETR_{\Ord}$ of elementary transfinite recursion for $\Ord$-length recursions of first-order properties, using any class parameter.

Implication cycle 12

We prove the theorem by establishing the complete cycle of indicated implications. The red arrows indicate more difficult or substantive implications, while the blue arrows indicate easier or nearly immediate implications. The green dashed implication from statement (12) to statement (1), while not needed for the completeness of the implication cycle, is nevertheless used in the proof that (12) implies (4). The proof of (12) implies (7) also uses (8), which follows from the fact that (12) implies (9) implies (8).

For more, download the paper from the arxiv:

  • V. Gitman, J. D. Hamkins, P. Holy, P. Schlicht, and K. Williams, “The exact strength of the class forcing theorem,” ArXiv e-prints, 2017. (manuscript under review)  
    @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 = {ArXiv e-prints},
    year = {2017},
    month = {July},
    volume = {},
    number = {},
    pages = {},
    note = {manuscript under review},
    abstract = {},
    keywords = {under-review},
    source = {},
    doi = {},
    eprint = {1707.03700},
    archivePrefix = {arXiv},
    primaryClass = {math.LO},
    url = {http://jdh.hamkins.org/class-forcing-theorem},
    }

See also Victoria’s post, Kameryn’s post.