Second-order transfinite recursion is equivalent to Kelley-Morse set theory over GBC

1167px-Wooden_spiral_stairs_(Nebotičnik,_Ljubljana)_croped
A few years ago, I had observed after hearing a talk by Benjamin Rin that the principle of first-order transfinite recursion for set well-orders is equivalent to the replacement axiom over Zermelo set theory, and thus we may take transfinite recursion as a fundamental set-theoretic principle, one which yields full ZFC when added to Zermelo’s weaker theory (plus foundation).

In later work, Victoria Gitman and I happened to prove that the principle of elementary transfinite recursion ETR, which allows for first-order class recursions along proper class well-orders (not necessarily set-like) is equivalent to the principle of determinacy for clopen class games [1]. Thus, once again, a strong recursion principle exhibited robustness as a fundamental set-theoretic principle.

The theme continued in recent joint work on the class forcing theorem, in which Victoria Gitman, myself, Peter Holy, Philipp Schlicht and Kameryn Williams [2] proved that the principle $\text{ETR}_{\text{Ord}}$, which allows for first-order class recursions of length $\text{Ord}$, is equivalent to twelve natural set-theoretic principles, including the existence of forcing relations for class forcing notions, the existence of Boolean completions for class partial orders, the existence of various kinds of truth predicates for infinitary logics, the existence of $\text{Ord}$-iterated truth predicates, and to the principle of determinacy for clopen class games of rank at most $\text{Ord}+1$.

A few days ago, a MathOverflow question of Alec Rhea’s — Is there a stronger form of recursion? — led me to notice that one naturally gains additional strength by pushing the recursion principles further into second-order set theory.

So let me introduce the second-order recursion principle STR and make the comparatively simple observation that over Gödel-Bernays GBC set theory this is equivalent to Kelley-Morse set theory KM. Thus, we may take this kind of recursion as a fundamental set-theoretic principle.

Definition. In the context of second-order set theory, the principle of second-order transfinite recursion, denoted STR, asserts of any formula $\varphi$ in the second-order language of set theory, that if $\Gamma=\langle I,\leq_\Gamma\rangle$ is any class well-order and $Z$ is any class parameter, then there is a class $S\subset I\times V$ that is a solution of the recursion, in the sense that
$$S_i=\{\ x\ \mid\  \varphi(x,S\upharpoonright i,Z)\ \}$$
for every $i\in I$, where where $S_i=\{\ x\ \mid\ (i,x)\in S\ \}$ is the section on coordinate $i$ and where $S\upharpoonright i=\{\ (j,x)\in S\ \mid\ j<_\Gamma i\ \}$ is the part of the solution at stages below $i$ with respect to $\Gamma$.

Theorem. The principle of second-order transfinite recursion STR is equivalent over GBC to the second-order comprehension principle. In other words, GBC+STR is equivalent to KM.

Proof. Kelley-Morse set theory proves that every second-order recursion has a solution in the same way that ZFC proves that every set-length well-ordered recursion has a solution. Namely, we simply consider the classes which are partial solutions to the recursion, in that they obey the recursive requirement, but possibly only on an initial segment of the well-order $\Gamma$. We may easily show by induction that any two such partial solutions agree on their common domain (this uses second-order comprehension in order to find the least point of disagreement, if any), and we can show that any given partial solution, if not already a full solution, can be extended to a partial solution on a strictly longer initial segment. Finally, we show that the common values of all partial solutions is therefore a solution of the recursion. This final step uses second-order comprehension in order to define what the common values are for the partial solutions to the recursion.

Conversely, the principle of second-order transfinite recursion clearly implies the second-order comprehension axiom, by considering recursions of length one. For any second-order assertion $\varphi$ and class parameter $Z$, we may deduce that $\{x\mid \varphi(x,Z)\}$ is a class, and so the second-order class comprehension principle holds. $\Box$

It is natural to consider various fragments of STR, such as $\Sigma^1_n\text{-}\text{TR}_\Gamma$, which is the assertion that every $\Sigma^1_n$-formula $\varphi$ admits a solution for recursions of length $\Gamma$.  Such principles are provable in proper fragments of KM, since for a given level of complexity, we only need a corresponding fragment of comprehension to undertake the proof that the recursion has a solution. The full STR asserts $\Sigma^1_\omega\text{-}\text{TR}$, allowing any length. The theorem shows that STR is equivalent to recursions of length $1$, since once you get the second-order comprehension principle, then you get solutions for recursions of any length. Thus, with second-order transfinite recursion, a little goes a long way. Perhaps it is more natural to think of transfinite recursion in this context not as axiomatizing KM, since it clearly implies second-order comprehension straight away, but rather as an apparent strengthening of KM that is actually provable in KM. This contrasts with the first-order situation of ETR with respect to GBC, where GBC+ETR does make a proper strengthening of GBC.

    • V. Gitman and J. D. Hamkins, “Open determinacy for class games,” in Foundations of Mathematics, Logic at Harvard, Essays in Honor of Hugh Woodin’s 60th Birthday, A. E. Caicedo, J. Cummings, P. Koellner, and P. Larson, Eds., American Mathematical Society, 2016. (also available as Newton Institute preprint ni15064)  
      @INCOLLECTION{GitmanHamkins2016:OpenDeterminacyForClassGames,
      author = {Victoria Gitman and Joel David Hamkins},
      title = {Open determinacy for class games},
      booktitle = {Foundations of Mathematics, Logic at Harvard, Essays in Honor of Hugh Woodin's 60th Birthday},
      publisher = {American Mathematical Society},
      year = {2016},
      editor = {Andr\'es E. Caicedo and James Cummings and Peter Koellner and Paul Larson},
      volume = {},
      number = {},
      series = {Contemporary Mathematics},
      type = {},
      chapter = {},
      pages = {},
      address = {},
      edition = {},
      month = {},
      note = {also available as Newton Institute preprint ni15064},
      url = {http://jdh.hamkins.org/open-determinacy-for-class-games},
      eprint = {1509.01099},
      archivePrefix = {arXiv},
      primaryClass = {math.LO},
      abstract = {},
      keywords = {},
      }

    • 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 = jul,
      volume = {},
      number = {},
      pages = {},
      note = {manuscript under review},
      abstract = {},
      keywords = {},
      source = {},
      doi = {},
      eprint = {1707.03700},
      archivePrefix = {arXiv},
      primaryClass = {math.LO},
      url = {http://jdh.hamkins.org/class-forcing-theorem},
      }

Photo by Petar Milošević (Own work) [CC BY-SA 4.0], via Wikimedia Commons

Open and clopen determinacy for proper class games, VCU MAMLS April 2017

This will be a talk for the Mid-Atlantic Mathematical Logic Seminar at Virginia Commonwealth University, a conference to be held April 1-2, 2017.

Richmond A line train bridge

Abstract. The principle of open determinacy for class games — two-player games of perfect information with plays of length $\omega$, where the moves are chosen from a possibly proper class, such as games on the ordinals — is not provable in Zermelo-Fraenkel set theory ZFC or Gödel-Bernays set theory GBC, if these theories are consistent, because provably in ZFC there is a definable open proper class game with no definable winning strategy. In fact, the principle of open determinacy and even merely clopen determinacy for class games implies Con(ZFC) and iterated instances Con(Con(ZFC)) and more, because it implies that there is a satisfaction class for first-order truth, and indeed a transfinite tower of truth predicates $\text{Tr}_\alpha$ for iterated truth-about-truth, relative to any class parameter. This is perhaps explained, in light of the Tarskian recursive definition of truth, by the more general fact that the principle of clopen determinacy is exactly equivalent over GBC to the principle of elementary transfinite recursion ETR over well-founded class relations. Meanwhile, the principle of open determinacy for class games is provable in the stronger theory GBC+$\Pi^1_1$-comprehension, a proper fragment of Kelley-Morse set theory KM. New work by Hachtman and Sato, respectively has clarified the separation of clopen and open determinacy for class games.

Lewis ChessmenThis is joint work with Victoria Gitman. See our article, Open determinacy for class games.

Slides

 

 

 

VCU MAMLS 2017

 

Regula Krapf, Ph.D. 2017, University of Bonn

Regula Krapf successfully defended her PhD dissertation January 12, 2017 at the University of Bonn, with a dissertation entitled, “Class forcing and second-order arithmetic.”  I was a member of the dissertation examining committee. Peter Koepke was the dissertation supervisor.

Regula Krapf

Regula Krapf, Class forcing and second-order arithmetic, dissertation 2017, University of Bonn. (Slides)

Abstract. We provide a framework in a generalization of Gödel-Bernays set theory for performing class forcing. The forcing theorem states that the forcing relation is a (definable) class in the ground model (definability lemma) and that every statement that holds in a class-generic extension is forced by a condition in the generic filter (truth lemma). We prove both positive and negative results concerning the forcing theorem. On the one hand, we show that the definability lemma for one atomic formula implies the forcing theorem for all formulae in the language of set theory to hold. Furthermore, we introduce several properties which entail the forcing theorem. On the other hand, we give both counterexamples to the definability lemma and the truth lemma. In set forcing, the forcing theorem can be proved for all forcing notions by constructing a unique Boolean completion. We show that in class forcing the existence of a Boolean completion is essentially equivalent to the forcing theorem and, moreover, Boolean completions need not be unique.

The notion of pretameness was introduced to characterize those forcing notions which preserve the axiom scheme of replacement. We present several new characterizations of pretameness in terms of the forcing theorem, the preservation of separation, the existence of nice names for sets of ordinals and several other properties. Moreover, for each of the aforementioned properties we provide a corresponding characterization of the Ord-chain condition.

Finally, we prove two equiconsistency results which compare models of ZFC (with large cardinal properties) and models of second-order arithmetic with topological regularity properties (and determinacy hypotheses). We apply our previous results on class forcing to show that many important arboreal forcing notions preserve the $\Pi^1_1$-perfect set property over models of second-order arithmetic and also give an example of a forcing notion which implies the $\Pi^1_1$-perfect set property to fail in the generic extension.

Regula has now taken up a faculty position at the University of Koblenz.

Ord is not definably weakly compact

  • A. Enayat and J. D. Hamkins, “ZFC proves that the class of ordinals is not weakly compact for definable classes.” (manuscript under review)  
    @ARTICLE{EnayatHamkins:Ord-is-not-definably-weakly-compact,
    author = {Ali Enayat and Joel David Hamkins},
    title = {{ZFC} proves that the class of ordinals is not weakly compact for definable classes},
    journal = {},
    year = {},
    volume = {},
    number = {},
    pages = {},
    month = {},
    note = {manuscript under review},
    abstract = {},
    keywords = {},
    source = {},
    doi = {},
    eprint = {1610.02729},
    archivePrefix = {arXiv},
    primaryClass = {math.LO},
    url = {http://jdh.hamkins.org/ord-is-not-definably-weakly-compact},
    }

In ZFC the class of all ordinals is very like a large cardinal.  Being closed under exponentiation, for example, Ord is a strong limit.  Indeed, it is a beth fixed point. And Ord is regular with respect to definable classes by the replacement axiom.  In this sense, ZFC therefore proves that Ord is definably inaccessible.  Which other large cardinal properties are exhibited by Ord? Perhaps you wouldn’t find it unreasonable for Ord to exhibit, at least consistently with ZFC, the definable proper class analogues of other much stronger large cardinal properties?

Meanwhile, the main results of this paper, joint between myself and Ali Enayat, show that such an expectation would be misplaced, even for comparatively small large cardinal properties. Specifically, in a result that surprised me, it turns out that the class of ordinals NEVER exhibits the definable proper class analogue of weak compactness in any model of ZFC.

Theorem. The class of ordinals is not definably weakly compact. In every model of ZFC:

  1. The definable tree property fails; there is a definable Ord-tree with no definable cofinal branch.
  2. The definable partition property fails; there is a definable 2-coloring of a definable proper class, with no homogeneous definable proper subclass.
  3. The definable compactness property fails for $\mathcal{L}_{\mathrm{Ord,\omega}}$; there is a definable theory in this logic, all of whose set-sized subtheories are satisfiable, but the whole theory has no definable class model.

The proof uses methods from the model theory of set theory, including especially the fact that no model of ZFC has a conservative $\Sigma_3$-elementary end-extension.

Theorem. The definable $\Diamond _{\mathrm{Ord}}$ principle holds in a model of ZFC if and only if the model has a definable well-ordering.

We close the paper by proving that the theory of the spartan models of Gödel-Bernays set theory GB — those equipped with only their definable classes — is $\Pi^1_1$-complete.

Theorem. The set of sentences true in all spartan models of GB is $\Pi_{1}^{1}$-complete.

The Vopěnka principle is inequivalent to but conservative over the Vopěnka scheme

  • J. D. Hamkins, “The Vopěnka principle is inequivalent to but conservative over the Vopěnka scheme.” (manuscript under review)  
    @ARTICLE{Hamkins:The-Vopenka-principle-is-inequivalent-to-but-conservative-over-the-Vopenka-scheme,
    author = {Joel David Hamkins},
    title = {The {Vop\v{e}nka} principle is inequivalent to but conservative over the {Vop\v{e}nka} scheme},
    journal = {},
    year = {},
    volume = {},
    number = {},
    pages = {},
    month = {},
    note = {manuscript under review},
    abstract = {},
    keywords = {},
    source = {},
    eprint = {1606.03778},
    archivePrefix = {arXiv},
    primaryClass = {math.LO},
    url = {http://jdh.hamkins.org/vopenka-principle-vopenka-scheme},
    }

Abstract. The Vopěnka principle, which asserts that every proper class of first-order structures in a common language admits an elementary embedding between two of its members, is not equivalent over GBC to the first-order Vopěnka scheme, which makes the Vopěnka assertion only for the first-order definable classes of structures. Nevertheless, the two Vopěnka axioms are equiconsistent and they have exactly the same first-order consequences in the language of set theory. Specifically, GBC plus the Vopěnka principle is conservative over ZFC plus the Vopěnka scheme for first-order assertions in the language of set theory.

Indras Net-03

The Vopěnka principle is the assertion that for every proper class $\mathcal{M}$ of first-order $\mathcal{L}$-structures, for a set-sized language $\mathcal{L}$, there are distinct members of the class $M,N\in\mathcal{M}$ with an elementary embedding $j:M\to N$ between them. In quantifying over classes, this principle is a single assertion in the language of second-order set theory, and it makes sense to consider the Vopěnka principle in the context of a second-order set theory, such as Godel-Bernays set theory GBC, whose language allows one to quantify over classes. In this article, GBC includes the global axiom of choice.

In contrast, the first-order Vopěnka scheme makes the Vopěnka assertion only for the first-order definable classes $\mathcal{M}$ (allowing parameters). This theory can be expressed as a scheme of first-order statements, one for each possible definition of a class, and it makes sense to consider the Vopěnka scheme in Zermelo-Frankael ZFC set theory with the axiom of choice.

Because the Vopěnka principle is a second-order assertion, it does not make sense to refer to it in the context of ZFC set theory, whose first-order language does not allow quantification over classes; one typically retreats to the Vopěnka scheme in that context. The theme of this article is to investigate the precise meta-mathematical interactions between these two treatments of Vopěnka’s idea.

Main Theorems.

  1. If ZFC and the Vopěnka scheme holds, then there is a class forcing extension, adding classes but no sets, in which GBC and the Vopěnka scheme holds, but the Vopěnka principle fails.
  2. If ZFC and the Vopěnka scheme holds, then there is a class forcing extension, adding classes but no sets, in which GBC and the Vopěnka principle holds.

It follows that the Vopěnka principle VP and the Vopěnka scheme VS are not equivalent, but they are equiconsistent and indeed, they have the same first-order consequences.

Corollaries.

  1. Over GBC, the Vopěnka principle and the Vopěnka scheme, if consistent, are not equivalent.
  2. Nevertheless, the two Vopěnka axioms are equiconsistent over GBC.
  3. Indeed, the two Vopěnka axioms have exactly the same first-order consequences in the language of set theory. Specifically, GBC plus the Vopěnka principle is conservative over ZFC plus the Vopěnka scheme for assertions in the first-order language of set theory. $$\text{GBC}+\text{VP}\vdash\phi\qquad\text{if and only if}\qquad\text{ZFC}+\text{VS}\vdash\phi$$

These results grew out of my my answer to a MathOverflow question of Mike Shulman, Can Vopěnka’s principle be violated definably?, inquiring whether there would always be a definable counterexample to the Vopěnka principle, whenever it should happen to fail. I interpret the question as asking whether the Vopěnka scheme is necessarily equivalent to the Vopěnka principle, and the answer is negative.

The proof of the main theorem involves the concept of a stretchable set $g\subset\kappa$ for an $A$-extendible cardinal, which has the property that for every cardinal $\lambda>\kappa$ and every extension $h\subset\lambda$ with $h\cap\kappa=g$, there is an elementary embedding $j:\langle V_\lambda,\in,A\cap V_\lambda\rangle\to\langle V_\theta,\in,A\cap V_\theta\rangle$ such that $j(g)\cap\lambda=h$. Thus, the set $g$ can be stretched by an $A$-extendibility embedding so as to agree with any given $h$.

Diamond on the ordinals

I was recently surprised to discover that if there is a definable well-ordering of the universe, then the diamond principle on the ordinals holds for definable classes, automatically. In fact, the diamond principle for definable classes is simply equivalent in ZFC to the existence of a definable well-ordering of the universe. It follows as a consequence that the diamond principle for definable classes, although seeming to be fundamentally scheme-theoretic, is actually expressible in the first-order language of set theory.

In set theory, the diamond principle asserts the existence of a sequence of objects $A_\alpha$, of growing size, such that any large object at the end is very often anticipated by these approximations.  In the case of diamond on the ordinals, what we will have is a definable sequence of $A_\alpha\subseteq\alpha$, such that for any definable class of ordinals $A$ and any definable class club set $C$, there are ordinals $\theta\in C$ with $A\cap\theta=A_\theta$.  This kind of principle typically allows one to undertake long constructions that will diagonalize against all the large objects, by considering and reacting to their approximations $A_\alpha$. Since every large object $A$ is often correctly approximated that way, this enables many such constructions to succeed.

Let me dive right in to the main part of the argument.$\newcommand\restrict\upharpoonright
\newcommand\of\subseteq
\newcommand\Ord{\text{Ord}}
\newcommand\HOD{\text{HOD}}\newcommand\ZFC{\text{ZFC}}$

Theorem. In $\ZFC$, if there is a definable well-ordering of the universe, then $\Diamond_{\Ord}$ holds for definable classes. That is, there is a $p$-definable sequence $\langle A_\alpha\mid\alpha<\Ord\rangle$, such that for any definable class $A\of\Ord$ and any definable closed unbounded class of ordinals $C\of\Ord$ (allowing parameters), there is some $\theta\in C$ with $A\cap\theta=A_\theta$.

Proof. The theorem is proved as a theorem scheme; namely, I shall provide a specific definition for the sequence $\vec A=\langle A_\alpha\mid\alpha<\Ord\rangle$, using the same parameter $p$ as the definition of the global well-order and with a definition of closely related syntactic complexity, and then prove as a scheme, a separate statement for each definable class $A\of\Ord$ and class club $C\of\Ord$, that there is some $\alpha\in C$ with $A\cap\alpha=A_\alpha$. The definitions of the classes $A$ and $C$ may involve parameters and have arbitrary complexity.

Let $\lhd$ be the definable well-ordering of the universe, definable by a specific formula using some parameter $p$. I define the $\Diamond_{\Ord}$-sequence $\vec A=\langle A_\alpha\mid\alpha<\Ord\rangle$ by transfinite recursion. Suppose that $\vec A\restrict\theta$ has been defined. I shall let $A_\theta=\emptyset$ unless $\theta$ is a $\beth$-fixed point above the rank of $p$ and there is a set $A\of\theta$ and a closed unbounded set $C\of\theta$, with both $A$ and $C$ definable in the structure $\langle V_\theta,\in\rangle$ (allowing parameters), such that $A\cap\alpha\neq A_\alpha$ for every $\alpha\in C$. In this case, I choose the least such pair $(A,C)$, minimizing first on the maximum of the logical complexities of the definitions of $A$ and of $C$, and then minimizing on the total length of the defining formulas of $A$ and $C$, and then minimizing on the Gödel codes of those formulas, and finally on the parameters used in the definitions, using the well-order $\lhd\restrict V_\theta$. For this minimal pair, let $A_\theta=A$. This completes the definition of the sequence $\vec A=\langle A_\alpha\mid\alpha\in\Ord\rangle$.

Let me remark on a subtle point, since the meta-mathematical issues loom large here. The definition of $\vec A$ is internal to the model, and at stage $\theta$ we ask about subsets of $\theta$ definable in $\langle V_\theta,\in\rangle$, using the truth predicate for this structure. If we were to run this definition inside an $\omega$-nonstandard model, it could happen that the minimal formula we get is nonstandard, and in this case, the set $A$ would not actually be definable by a standard formula. Also, even when $A$ is definable by a standard formula, it might be paired (with some constants), with a club set $C$ that is defined only by a nonstandard formula (and this is why we minimize on the maximum of the complexities of the definitions of $A$ and $C$ together). So one must give care in the main argument keeping straight the distinction between the meta-theoretic natural numbers and the internal natural numbers of the object theory $\ZFC$.

Let me now prove that the sequence $\vec A$ is indeed a $\Diamond_{\Ord}$-sequence for definable classes. The argument follows in spirit the classical proof of $\Diamond$ in $L$, subject to the mathematical issues I mentioned. If the sequence $\vec A$ is not a diamond sequence, then there is some definable class $A\of\Ord$, defined in $\langle V,\in\rangle$ by a specific formula $\varphi$ and parameter $z$, and definable club $C\of\Ord$, defined by some $\psi$ and parameter $y$, with $A\cap\alpha\neq A_\alpha$ for every $\alpha\in C$. We may assume without loss that these formulas are chosen so as to be minimal in the sense of the construction, so that the maximum of the complexities of $\varphi$ and $\psi$ are as small as possible, and the lengths of the formulas, and the Gödel codes and finally the parameters $z,y$ are $\lhd$-minimal, respectively, successively. Let $m$ be a sufficiently large natural number, larger than the complexity of the definitions of $\lhd$, $A$, $C$, and large enough so that the minimality condition we just discussed is expressible by a $\Sigma_m$ formula. Let $\theta$ be any $\Sigma_m$-correct ordinal above the ranks of the parameters used in the definitions. It follows that the restrictions $\lhd\restrict V_\theta$ and also $A\cap\theta$ and $C\cap\theta$ and $\vec A\restrict\theta$ are definable in $\langle V_\theta,\in\rangle$ by the same definitions and parameters as their counterparts in $V$, that $C\cap\theta$ is club in $\theta$, and that $A\cap\theta$ and $C\cap\theta$ form a minimal pair using those definitions with $A\cap\alpha\neq A_\alpha$ for any $\alpha\in C\cap\theta$. Thus, by the definition of $\vec A$, it follows that $A_\theta=A\cap\theta$. Since $C\cap\theta$ is unbounded in $\theta$ and $C$ is closed, it follows that $\theta\in C$, and so $A_\theta=A\cap\theta$ contradicts our assumption about $A$ and $C$. So there are no such counterexample classes, and thus $\vec A$ is a $\Diamond_{\Ord}$-sequence with respect to definable classes, as claimed.
QED

Theorem. The following are equivalent over $\ZFC$.

  1. There is a definable well-ordering of the universe, using some set parameter $p$.
  2. $V=\HOD_{\{p\}}$, for some set $p$.
  3. $\Diamond_{\Ord}$ holds for definable classes. That is, there is a set parameter $p$ and a definable sequence $\vec A=\langle A_\alpha\mid\alpha<\Ord\rangle$, such that for any definable class $A\of\Ord$ and definable class club $C\of\Ord$, there is some $\alpha\in C$ with $A\cap\alpha=A_\alpha$.

Proof. Let me first give the argument, and then afterward discuss some issues about the formalization, which involves some subtle issues.

($1\to 2$) $\newcommand\rank{\text{rank}}$Suppose that $\lhd$ is a $p$-definable well-ordering of $V$, which means that every set has a $\lhd$-minimal element. Let us refine this order by defining $x\lhd’ y$, just in case $\rank(x)<\rank(y)$ or $\rank(x)=\rank(y)$ and $x\lhd y$. The new order is also a well-order, which now respects rank. In particular, the order $\lhd’$ is set-like, and so every object $x$ is the $\alpha^{th}$ element with respect to the $\lhd’$-order, for some ordinal $\alpha$. Thus, every object is definable from $p$ and an ordinal, and so $V=\HOD_{\{p\}}$, as desired.

($2\to 1$) If $V=\HOD_{\{p\}}$, then we have the canonical well-order of $\HOD$ using parameter $p$, similar to how one shows that the axiom of choice holds in $\HOD$. Namely, define $x\lhd y$ if and only if $\rank(x)<\rank(y)$, or the ranks are the same, but $x$ is definable from $p$ and ordinal parameters in some $V_\theta$ with a smaller $\theta$ than $y$ is, or the ranks are the same and the $\theta$ is the same, but $x$ is definable in that $V_\theta$ by a formula with a smaller Gödel code, or with the same formula but smaller ordinal parameters. It is easy to see that this is a $p$-definable well-ordering of the universe.

($1\to 3$) This is the content of the theorem above.

($3\to 1$) If $\vec A$ is a $p$-definable $\Diamond_{\Ord}$-sequence for definable classes, then it is easy to see that if $A$ is a set of ordinals, then $A$ must arise as $A_\alpha$ for unboundedly many $\alpha$. In $\ZFC$, using the axiom of choice, it is a standard fact that every set is coded by a set of ordinals. So let us define that $x\lhd y$, just in case $x$ is coded by a set of ordinals that appears earlier on $\vec A$ than any set of ordinals coding $y$. This is clearly a well-ordering, since the map sending $x$ to the ordinal $\alpha$ for which $A_\alpha$ codes $x$ is an $\Ord$-ranking of $\lhd$. So there is a $p$-definable well-ordering of the universe.
QED

An observant reader will notice some meta-mathematical issues concerning the previous theorem. The issue is that statements 1 and 2 are known to be expressible by statements in the first-order language of set theory, as single statements, but for statement 3 we have previously expressed it only as a scheme of first-order statements. So how can they be equivalent? The answer is that the full scheme-theoretic content of statement 3 follows already from instances in which the complexity of the definitions of $A$ and $C$ are bounded. Basically, once one gets the global well-order, then one can construct a $\Diamond_{\Ord}$-sequence that works for all definable classes. In this sense, we may regard the diamond principle $\Diamond_{\Ord}$ for definable classes as not really a scheme of statements, but rather equivalent to a single first-order assertion.

Lastly, let me consider the content of the theorems in Gödel-Bernays set theory or Kelley-Morse set theory. Of course, we know that there can be models of these theories that do not have $\Diamond_{\Ord}$ in the full second-order sense. For example, it is relatively consistent with ZFC that an inaccessible cardinal $\kappa$ does not have $\Diamond_\kappa$, and in this case, the structure $\langle V_\kappa,\in,V_{\kappa+1}\rangle$ will satisfy GBC and even KM, but it won’t have $\Diamond_{\Ord}$ with respect to all classes, even though it has a definable well-ordering of the universe (since there is such a well-ordering in $V_{\kappa+1}$). But meanwhile, there will be a $\Diamond_{\Ord}$-sequence that works with respect to classes that are definable from that well-ordering and parameters, simply by following the construction given in the theorem.

This leads to several extremely interesting questions, about which I am currently thinking, concerning instances where we can have $\Diamond_\kappa$ for definable classes in $V_\kappa$, even when the full $\Diamond_\kappa$ fails. Stay tuned!

Open determinacy for games on the ordinals is stronger than ZFC, CUNY Logic Workshop, October 2015

This will be a talk for the CUNY Logic Workshop on October 2, 2015.

Abstract. The principle of open determinacy for class games — two-player games of perfect information with plays of length $\omega$, where the moves are chosen from a possibly proper class, such as games on the ordinals — is not provable in Zermelo-Fraenkel set theory ZFC or Gödel-Bernays set theory GBC, if these theories are consistent, because provably in ZFC there is a definable open proper class game with no definable winning strategy. In fact, the principle of open determinacy and even merely clopen determinacy for class games implies Con(ZFC) and iterated instances Con(Con(ZFC)) and more, because it implies that there is a satisfaction class for first-order truth, and indeed a transfinite tower of truth predicates $\text{Tr}_\alpha$ for iterated truth-about-truth, relative to any class parameter. This is perhaps explained, in light of the Tarskian recursive definition of truth, by the more general fact that the principle of clopen determinacy is exactly equivalent over GBC to the principle of elementary transfinite recursion ETR over well-founded class relations. Meanwhile, the principle of open determinacy for class games is provable in the stronger theory GBC+$\Pi^1_1$-comprehension, a proper fragment of Kelley-Morse set theory KM.

This is joint work with Victoria Gitman, with the helpful participation of Thomas Johnstone.

Related article and posts:

 

 

Open determinacy for class games

  • V. Gitman and J. D. Hamkins, “Open determinacy for class games,” in Foundations of Mathematics, Logic at Harvard, Essays in Honor of Hugh Woodin’s 60th Birthday, A. E. Caicedo, J. Cummings, P. Koellner, and P. Larson, Eds., American Mathematical Society, 2016. (also available as Newton Institute preprint ni15064)  
    @INCOLLECTION{GitmanHamkins2016:OpenDeterminacyForClassGames,
    author = {Victoria Gitman and Joel David Hamkins},
    title = {Open determinacy for class games},
    booktitle = {Foundations of Mathematics, Logic at Harvard, Essays in Honor of Hugh Woodin's 60th Birthday},
    publisher = {American Mathematical Society},
    year = {2016},
    editor = {Andr\'es E. Caicedo and James Cummings and Peter Koellner and Paul Larson},
    volume = {},
    number = {},
    series = {Contemporary Mathematics},
    type = {},
    chapter = {},
    pages = {},
    address = {},
    edition = {},
    month = {},
    note = {also available as Newton Institute preprint ni15064},
    url = {http://jdh.hamkins.org/open-determinacy-for-class-games},
    eprint = {1509.01099},
    archivePrefix = {arXiv},
    primaryClass = {math.LO},
    abstract = {},
    keywords = {},
    }

Abstract. The principle of open determinacy for class games — two-player games of perfect information with plays of length $\omega$, where the moves are chosen from a possibly proper class, such as games on the ordinals — is not provable in Zermelo-Fraenkel set theory ZFC or Godel-Bernays set theory GBC, if these theories are consistent, because provably in ZFC there is a definable open proper class game with no definable winning strategy. In fact, the principle of open determinacy and even merely clopen determinacy for class games implies Con(ZFC) and iterated instances Con(Con(ZFC)) and more, because it implies that there is a satisfaction class for first-order truth, and indeed a transfinite tower of truth predicates $\text{Tr}_\alpha$ for iterated truth-about-truth, relative to any class parameter. This is perhaps explained, in light of the Tarskian recursive definition of truth, by the more general fact that the principle of clopen determinacy is exactly equivalent over GBC to the principle of transfinite recursion over well-founded class relations. Meanwhile, the principle of open determinacy for class games is provable in the stronger theory GBC$+\Pi^1_1$-comprehension, a proper fragment of Kelley-Morse set theory KM.

See my earlier posts on part of this material:

 

Determinacy for proper-class clopen games is equivalent to transfinite recursion along proper-class well-founded relations

The Infinite Combat - Philipp Klinger

I’d like to continue a bit further my exploration of some principles of determinacy for proper-class games; it turns out that these principles have a surprising set-theoretic strength.  A few weeks ago, I explained that the determinacy of proper-class open games and even clopen games implies Con(ZFC) and much more.  Today, I’d like to prove that clopen determinacy is exactly equivalent over GBC to the principle of transfinite recursion along proper-class well-founded relations.  Thus, GBC plus either of these principles is a strictly intermediate set theory between GBC and KM.

The principle of clopen determinacy for class games is the assertion that in any two-player infinite game of perfect information whose winning condition is a clopen class, there is a winning strategy for one of the players. Players alternately play moves in a playing space $X$, thereby creating a particular play $\vec a\in X^\omega$, and the winner is determined according to whether $\vec a$ is in a certain fixed payoff class $U\subset X^\omega$ or not. One has an open game when this winning condition class $U$ is open in the product topology (using the discrete topology on $X$). A game is open for a player if and only if every winning play for that player has an initial segment, all of whose extensions are also winning for that player. So the game is won for an open player at a finite stage of play. A clopen game, in contrast, has a payoff set that is open for both players. Clopen games can be equivalently cast in terms of the game tree, consisting of positions in the game where the winner is not yet determined, and where play terminates when the winner is known. Namely, a game is clopen exactly when this game tree is well-founded, so that in every play, the outcome is known already at a finite stage.

A strategy is a class function $\sigma:X^{<\omega}\to X$ that instructs the player what to play next, given a position of partial play, and the strategy is winning for a player if all plays that accord with it satisfy the winning condition for that player.

The principle of transfinite recursion along well-founded class relations is the assertion that we may undertake recursive definitions along any class well-founded partial order relation. That is, suppose that $\lhd$ is a class well-founded partial order relation on a class $A$, and suppose that $\varphi(F,a,y)$ is a formula, using only first-order quantifiers but having a class variable $F$, which is functional in the sense that for any class $F$ and any set $a\in A$ there is a unique $y$ such that $\varphi(F,a,y)$. The idea is that $\varphi(F,a,y)$ expresses the recursive rule to be iterated, and a solution of the recursion is a class function $F$ such that $\varphi(F\upharpoonright a,a,F(a))$ holds for every $a\in A$, where $F\upharpoonright a$ means the restriction of $F$ to the class $\{ b\in A\mid b\lhd a\}$. Thus, the value $F(a)$ is determined by the class of previous values $F(b)$ for $b\lhd a$. The principle of transfinite recursion along class well-founded relations is the assertion scheme that for every such well-founded partial order class $\langle A,\lhd\rangle$ and any recursive rule $\varphi$ as above, there is a solution.

In the case that the relation $\lhd$ is set-like, which means that the predecessors $\{b\mid b\lhd a\}$ of any point $a$ form a set (rather than a proper class), then GBC easily proves that there is a unique solution class, which furthermore is definable from $\lhd$. Namely, one can show that every $a\in A$ has a partial solution that obeys the recursive rule at least up to $a$, and furthermore all such partial solutions agree below $a$, because there can be no $\lhd$-minimal violation of this. It follows that the class function $F$ unifying these partial solutions is a total solution to the recursion. Similarly, GBC can prove that there are solutions to other transfinite recursion instances where the well-founded relation is not necessarily set-like, such as a recursion of length $\text{Ord}+\text{Ord}$ or even much longer.

Meanwhile, if GBC is consistent, then it cannot in general prove that transfinite recursions along non-set-like well-founded relations always succeed, since this principle would imply that there is a truth-predicate for first-order truth, as the Tarskian conditions are precisely such a recursion on a well-founded relation based on the complexity of formulas. (That relation is not set-like, since when considering the truth of $\exists x\,\psi(x,\vec a)$, we want to consider the truth of $\psi(b,\vec a)$ for any parameter $b$, and there are a proper class of such $b$.) Thus, GBC plus transfinite recursion (or plus clopen determinacy) is strictly stronger than GBC, although it is provable in Kelley-Morse set theory KM essentially the same as GBC proves the set-like special case.

Theorem. Assume GBC. Then the following are equivalent.

  1. Clopen determinacy for class games. That is, for any two-player game of perfect information whose payoff class is both open and closed, there is a winning strategy for one of the players.
  2. Transfinite recursion for proper class well-founded relations (not necessarily set-like).

Proof. ($2\to 1$) Assume the principle of transfinite recursion for proper class well-founded relations, and suppose we are faced with a clopen game. Consider the game tree $T$, consisting of positions arising during play, up to the moment that a winner is known. This tree is well-founded because the game is clopen. Let us label the terminal nodes of the tree with I or II according to who has won the game in that position, and more generally, let us label all the nodes of the tree with I or II according to the following transfinite recursion: if a node has I to play, then it will have label I if there is a move to a node labeled I, and otherwise II; and similarly when it is II to play. By the principle of transfinite recursion, there is a labeling of the entire tree that accords with this recursive rule. It is now easy to see that if the initial node is labeled with I, then player I has a winning strategy, which is simply to stay on the nodes labeled I. Note that player II cannot play in one move from a node labeled I to one labeled II. Similarly, if the initial node is labeled II, then player II has a winning strategy; and so the game is determined, as desired.

($1\to 2$) Conversely, let us assume the principle of clopen determinacy for class games. Suppose we are faced with a recursion along a class relation $\lhd$ on a class $A$, using a recursion rule $\varphi(F,a,y)$. We shall define a certain clopen game, and prove that any winning strategy for this game will produce a solution for the recursion.

It will be convenient to assume that $\varphi(F,a,y)$ is strongly functional, meaning that not only does it define a function as we have mentioned in $V$, but also that $\varphi(F,a,y)$ defines a function $(F,a)\mapsto y$ when used over any model $\langle V_\theta,\in,F\rangle$ for any class $F\subset V_\theta$. The strongly functional property can be achieved simply by replacing the formula with the assertion that $\varphi(F,a,y)$, if $y$ is unique such that this holds, and otherwise $y=\emptyset$.

At first, let us consider a slightly easier game, which will be open rather than clopen; a bit later, we shall revise this game to a clopen game. The game is the recursion game, which will be very much like the truth-telling game of my previous post, Open determinacy for proper class games implies Con(ZFC) and much more. Namely, we have two players, the challenger and the truth-teller. The challenger will issues challenges about truth in a structure $\langle V,\in,\lhd,F\rangle$, where $\lhd$ is the well-founded class relation and $F$ is a class function, not yet specified. Specifically, the challenger is allowed to ask about the truth of any formula $\varphi(\vec a)$ in this structure, and to inquire as to the value of $F(a)$ for any particular $a$. The truth-teller, as before, will answer the challenges by saying either that $\varphi(\vec a)$ is true or false, and in the case $\varphi(\vec a)=\exists x\,\psi(x,\vec a)$ and the formula was declared true, by also giving a witness $b$ and declaring $\psi(b,\vec a)$ is true; and the truth-teller must specify a specific value for $F(a)$ for any particular $a$. The truth-teller loses immediately, if she should ever violate Tarski’s recursive definition of truth; and she also loses unless she declares the recursive rules $\varphi(F\upharpoonright a,a,F(a))$ to be true. Since these violations occur at a finite stage of play if they do at all, the game is open for the challenger.

Lemma. The challenger has no winning strategy in the recursion game.

Proof. Suppose that $\sigma$ is a strategy for the challenger. So $\sigma$ is a class function that instructs the challenger how to play next, given a position of partial play. By the reflection theorem, there is an ordinal $\theta$ such that $V_\theta$ is closed under $\sigma$, and using the satisfaction class that comes from clopen determinacy, we may actually also arrange that $\langle V_\theta,\in,\lhd\cap V_\theta,\sigma\cap V_\theta\rangle\prec\langle V,\in,\lhd,\sigma\rangle$. Consider the relation $\lhd\cap V_\theta$, which is a well-founded relation on $A\cap V_\theta$. The important point is that this relation is now a set, and in GBC we may certainly undertake transfinite recursions along well-founded set relations. Thus, there is a function $f:A\cap V_\theta\to V_\theta$ such that $\langle V_\theta,\in,f\rangle$ satisfies $\varphi(f\upharpoonright a,a,f(a))$ for all $a\in V_\theta$, where $f\upharpoonright a$ means restricting $f$ to the predecessors of $a$ in $V_\theta$, and this may not be all the predecessors of $a$ with respect to $\lhd$, which may not be set-like. Note that this is the place where we use our assumption that $\varphi$ was strongly functional, since we want to ensure that it can still be used to define a valid recursion over $\lhd\cap V_\theta$. (We are not claiming that $\langle V_\theta,\in,\lhd\cap V_\theta,f\rangle$ models $\text{ZFC}(\lhd,f)$.)

Consider now the play of the recursion game in $V$, where the challenger uses the strategy $\sigma$ and the truth-teller plays in accordance with $\langle V_\theta,\in,\lhd\cap V_\theta,f\rangle$. Since $V_\theta$ was closed under $\sigma$, the challenger will never issue challenges outside of $V_\theta$. And since the function $f$ fulfills the recursion $\varphi(f\upharpoonright a,a,f(a))$ in this structure, the truth-teller will not be trapped in any violation of the Tarski conditions or the recursion condition. Thus, the truth-teller will win this instance of the game, and so $\sigma$ was not a winning strategy for the challenger, as desired. QED

Lemma. The truth-teller has a winning strategy in the recursion game if and only if there is a solution of the recursion.

Proof. If there is a solution $F$ of the recursion, then by clopen determinacy, we also get a satisfaction class for the structure $\langle V,\in,\lhd,F\rangle$, and the truth-teller can answer all queries of the challenger by referring to what is actually true in this structure. This will be winning for the truth-teller, since the actual truth obeys the Tarskian conditions and the recursive rule.

Conversely, suppose that $\tau$ is a winning strategy for the truth-teller in the recursion game. We claim that the truth assertions made by $\tau$ do not depend on the order in which challenges are made by the challenger; they all cohere with one another. This is easy to see for formulas not involving $F$ by induction on formulas, for if the truth of a formula $\psi(\vec a)$ is independent of play, then also the truth of $\neg\psi(\vec a)$ is as well, and similarly if $\exists x\psi(x,\vec a)$ is declared true with witness $\psi(b,\vec a)$, then by induction $\psi(b,\vec a)$ is independent of the play, in which case $\exists x\psi(x,\vec a)$ must always be declared true by $\tau$ independently of the order of play by the challenger (although the particular witness $b$ provided by $\tau$ may depend on the play). Now, let us also argue that the values of $F(a)$ declared by $\tau$ are also independent of the order of play. If not, there is some $\lhd$-least $a$ where this fails. (Note that such an $a$ exists, since $\tau$ is a class, and we can define from $\tau$ the class of $a$ for which the value of $F(a)$ declared by $\tau$ depends on the order of play; without $\tau$, one might have expected to need $\Pi^1_1$-comprehension to find a minimal $a$ where the recursion fails.) As in the truth-telling game, the truth assertions made by $\tau$ about $\langle V,\in,\lhd,F\upharpoonright a\rangle$, where $F\upharpoonright a$ is the class function of values that are determined by $\tau$ on $b\lhd a$, must not depend on the order of play. Since the recursion rule $\varphi(F\upharpoonright a,a,y)$ is functional, there is only one value $y=F(a)$ for which this formula can be truthfully held, and so if some play causes $\tau$ to play a different value for $F(a)$, the challenger can in finitely many additional moves (bounded by the syntactic complexity of $\varphi$) trap the truth-teller in a violation of the Tarskian conditions or the recursion condition. Thus, the values of $F(a)$ declared by $\tau$ must in fact all cohere independently of the order of play, and so $\tau$ is describing a class function $F:A\to V$ such that $\varphi(F\upharpoonright a,a,F(a))$ is true for every $a\in A$. So the recursion has a solution, as desired. QED

So far, we have established that the principle of open determinacy implies the principle of transfinite recursion along well-founded class relations. In order to improve this implication to use only clopen determinacy rather than open determinacy, we modify the game to become a clopen game rather than an open game.

Consider the clopen form of the recursion game, where we insist also that the challenger announce on the first move a natural number $n$, such that the challenger loses if the truth-teller survives for at least $n$ moves. This is now a clopen game, since the winner will be known by that time, either because the truth-teller will violate the Tarski conditions or the recursion condition, or else the challenger’s limit on play will expire.

Since the modified version of the game is even harder for the challenger, there can still be no winning strategy for the challenger. So by the principle of clopen determinacy, there is a winning strategy $\tau$ for the truth-teller. This strategy is allowed to make decisions based on the number $n$ announced by the challenger on the first move, and it will no longer necessarily be the case that the theory declared true by $\tau$ will be independent of the order of play. Nevertheless, it will be the case, we claim, that the theory declared true by $\tau$ for all plays with sufficiently large $n$ (and with sufficiently many remaining moves) will be independent of the order of play. One can see this by observing that if an assertion $\psi(\vec a)$ is independent in this sense, then also $\neg\psi(\vec a)$ will be independent in this sense, for otherwise there would be plays with large $n$ giving different answers for $\neg\psi(\vec a)$ and we could then challenge with $\psi(\vec a)$, which would have to give different answers or else $\tau$ would not win. Similarly, since $\tau$ is winning, one can see that allowing the challenger to specify a bound on the total length of play does not prevent the arguments above showing that $\tau$ describes a coherent solution function $F:A\to V$ satisfying the recursion $\varphi(F\upharpoonright a,a,F(a))$, provided that one looks only at plays in which there are sufficiently many moves remaining. There cannot be a $\lhd$-least $a$ where the value of $F(a)$ is not determined in this sense, and so on as before.

Thus, we have proved that the principle of clopen determinacy for class games is equivalent to the principle of transfinite recursion along well-founded class relations. QED

The material in this post will become part of a joint project with Victoria Gitman and Thomas Johnstone. We are currently investigating several further related issues.

Open determinacy for proper class games implies Con(ZFC) and much more

1000px-Apollonian_gasket.svg

$\newcommand\Tr{\text{Tr}}$One of the intriguing lessons we have learned in the past half-century of set-theoretic developments is that there is a surprisingly robust connection between infinitary game theory and fundamental set-theoretic principles, including large cardinals. Assertions about the existence of strategies in infinite games often turn out to have an unexpected set-theoretic power. In this post, I should like to give another specific example of this, which Thomas Johnstone and I hit upon yesterday in an enjoyable day of mathematics.

Specifically, I’d like to prove that if we generalize the open-game concept from sets to classes, then assuming consistency, ZFC cannot prove that every definable open class game is determined, and indeed, over Gödel-Bernays set theory GBC the principle of open determinacy (and even just clopen determinacy) implies Con(ZFC) and much more.

To review a little, we are talking about games of perfect information, where two players alternately play elements from an allowed space $X$ of possible moves, and together they build an infinite sequence $\vec x=\langle x_0,x_1,x_2,\ldots\rangle$ in $X^\omega$, which is the resulting play of this particular instance of the game. We have a fixed collection of plays $A\subset X^\omega$ that is used to determine the winner, namely, the first player wins this particular instance of the game if the resulting play $\vec x$ is in $A$, and otherwise the second player wins. A strategy for a player is a function $\sigma:X^{<\omega}\to X$, which tells a player how to move next, given a finite position in the game. Such a strategy is winning for that player, if he or she always wins by following the instructions, no matter how the opponent plays. The game is determined, if one of the players has a winning strategy.

It is a remarkable but elementary fact that if the winning condition $A$ is an open set, then the game is determined. One can prove this by using the theory of ordinal game values, and my article on transfinite game values in infinite chess contains an accessible introduction to the theory of game values. Basically, one defines that a position has game value zero (for player I, say), if the game has already been won at that stage, in the sense that every extension of that position is in the winning payoff set $A$. A position with player I to play has value $\alpha+1$, if player I can move to a position with value $\alpha$, and $\alpha$ is minimal. The value of a position with player II to play is the supremum of the values of all the positions that he or she might reach in one move, provided that those positions have a value. The point now is that if a position has a value, then player I can play so as strictly to decrease the value, and player II cannot play so as to increase it. So if a position has a value, then player I has a winning strategy, which is the value-reducing strategy. Conversely, if a position does not have a value, then player II can maintain that fact, and player I cannot play so as to give it a value; thus, in this case player II has a winning strategy, the value-maintaining strategy. Thus, we have proved the Gale-Stewart theorem: every open game is determined.

That proof relied on the space of moves $X$ being a set, since we took a supremum over the values of the possible moves, and if $X$ were a proper class, we couldn’t be sure to stay within the class of ordinals and the recursive procedure might break down. What I’d like to do is to consider more seriously the case where $X$ is a proper class. Similarly, we allow the payoff collection $A$ to be a proper class, and the strategies $\sigma:X^{<\omega}\to X$ are also proper classes. Can we still prove the Gale-Steward theorem for proper classes? The answer is no, unless we add set-theoretic strength. Indeed, even clopen determinacy has set-theoretic strength.

Theorem. (GBC) Clopen determinacy for proper classes implies Con(ZFC) and much more. Specifically, there is a clopen game, such the existence of a winning strategy is equivalent to the existence of a satisfaction class for first-order truth.

Proof. Let me first describe a certain open game, the truth-telling game, with those features, and I shall later modify it to a clopen game. The truth-telling game will have two players, which I call the challenger and the truth-teller. At any point in the game, the challenger plays by making an inquiry about a particular set-theoretic formula $\varphi(\vec a)$ with parameters. The truth-teller must reply to the inquiry by stating either true or false, and in the case that the formula $\varphi$ is an existential assertion $\exists x\,\psi(x,\vec a)$ declared to be true, then the truth teller must additionally identify a particular witness $b$ and assert that $\psi(b,\vec a)$ is true. So a play of the game consists of a sequence of such inquires and replies.

The truth-teller wins a play of the game, provided that she never violates the recursive Tarskian truth conditions. Thus, faced with an atomic formula, she must state true or false in accordance with the actual truth or falsity of that atomic formula, and similarly,
she must say true to $\varphi\wedge\psi$ just in case she said true to both $\varphi$ and $\psi$ separately (if those formulas had been issued by the challeger), and she must state opposite truth values for $\varphi$ and $\neg\varphi$, if both are issued as challenges.

This is an open game, since the challenger will win, if at all, at a finite stage of play, when the violation of the Tarskian truth conditions is first exhibited.

Lemma 1. The truth-teller has a winning strategy in the truth-telling game if and only if there is a satisfaction class for first-order truth.

Proof. Clearly, if there is a satisfaction class for first-order truth, then the truth-teller has a winning strategy, which is simply to answer all questions about truth by consulting the
satisfaction class. Since that class obeys the Tarskian conditions, she will win the game, no matter which challenges are issued.

Conversely, suppose that the truth-teller has a winning strategy $\tau$ in the game. I claim that we may use $\tau$ to build a satisfaction class for first-order truth. Specifically, let $T$ be the collection of formulas $\varphi(\vec a)$ that are asserted to be true by $\tau$ in any play according to $\tau$. I claim that $T$ is a satisfaction class. We may begin by noting that since $T$ must correctly state the truth of all atomic formulas, it follows that the particular answers that $\tau$ gives on the atomic formulas does not depend on the order of the challenges issued by the challenger. Now, we argue by induction on formulas that the truth values issued by $\tau$ does not depend on the order of the challenges. For example, if all plays in which $\varphi(\vec a)$ is issued as a challenge come out true, then all plays in which $\neg\varphi(\vec a)$ is challenged will result in false, or else we would have a play in which $\tau$ would violate the Tarskian truth conditions. Similarly, if $\varphi$ and $\psi$ always come out the same way, then so does $\varphi\wedge\psi$. We don’t claim that $\tau$ must always issue the same witness $b$ for an existential $\exists x\,\psi(x,\vec a)$, but if it ever says true to this statement, then it will provide some witness $b$, and for that statement $\psi(b,\vec a)$, the truth value stated by $\tau$ is independent of the order of play by the challenger, by induction. Thus, by induction on formulas, the answers provided by the truth-teller strategy $\tau$ gives us a satisfaction predicate for first-order truth. QED

Lemma 2. The challenger has no winning strategy in the truth-telling game.

Proof. Suppose that $F$ is a strategy for the challenger. So $F$ is a proper class function that directs the challenger to issue certain challenges, given the finite sequence of previous challenges and truth-telling answers. By the reflection theorem, there is a closed unbounded proper class of cardinals $\theta$, such that $F”V_\theta\subset V_\theta$. That is, $V_\theta$ is closed under $F$, in the sense that if all previous challenges and responses come from $V_\theta$, then the next challenge will also come from $V_\theta$. Since $\langle V_\theta,\in\rangle$ is a set, we have a satisfaction predicate on it. Consider the play, where the truth-teller replies to all inquires by consulting truth in $V_\theta$, rather than truth in $V$. The point is that if the challenger follows $\tau$, then all the inquiries will involve only parameters $\vec a$ in $V_\theta$, provided that the truth-teller also always gives witnesses in $V_\theta$, which in this particular play will be the case. Since the satisfaction predicate on $V_\theta$ does satisfy the Tarskian truth conditions, it follows that the truth-teller will win this instance of the game, and so $F$ is not a winning strategy for the challenger. QED

Thus, if open determinacy holds for classes, then there is a satisfaction predicate for first-order truth.

This implies Con(ZFC) for reasons I explained on my post KM implies Con(ZFC) and much more, by appealing to the fact that we have the collection axiom relative to the class for the satisfaction predicate itself, and this is enough to verify that the nonstandard instances of collection also must be declared true in the satisfaction predicate.

But so far, we only have an open game, rather than a clopen game, since the truth-teller wins only by playing the game out for infinitely many steps. So let me describe how to modify the game to be clopen. Specifically, consider the version of the truth-telling game, where the challenger must also state on each move a specific ordinal $\alpha_n$, which descend during play $\alpha_0>\alpha_1>\cdots>\alpha_n$. If the challenger gets to $0$, then the truth-teller is declared the winner. For this modified game, the winner is known in finitely many moves, because either the truth-teller violates the Tarskian conditions or the challenger hits zero. So this is a clopen game. Since we made the game harder for the challenger, it follows that the challenger still can have no winning strategy. One can modify the proof of lemma 1 to say that if $\tau$ is a winning strategy for the truth teller, then the truth assertions made by $\tau$ in response to all plays with sufficiently large ordinals for the challenger all agree with one another independently of the order of the formulas issued by the challenger. Thus, there is a truth-telling strategy just in case there is a satisfaction class for first-order truth.

So clopen determinacy for class games implies the existence of a satisfaction class for first-order truth, and this implies Con(ZFC) and much more. QED

One may easily modify the game by allowing a fixed class parameter $B$, so that clopen determinacy implies that there is a satisfaction class relative to truth in $\langle V,\in,B\rangle$.

Furthermore, we may also get iterated truth predicates. Specifically, consider the iterated truth-telling game, which in addition to the usual language of set theory, we have a hierarchy of predicates $\Tr_\alpha$ for any ordinal $\alpha$. We now allow the challenger to ask about formulas in this expanded language, and the truth teller is required to obey not only the usual Tarskian recursive truth conditions, but also the requirements that $\Tr_\alpha(\varphi(\vec a))$ is declared true just in case $\varphi(\vec a)$ uses only truth predicates $\Tr_\beta$ for $\beta<\alpha$ and also $\varphi(\vec a)$ is declared true (if this challenge was issued).

The main arguments as above generalize easily to show that the challenger cannot have a winning strategy in this iterated truth-telling game, and the truth-teller has a strategy just in case there is a satisfaction predicate for truth-about-truth iterated through the ordinals.  Thus, the principle of open determinacy for proper class games implies Con(Con(ZFC)) and $\text{Con}^\alpha(\text{ZFC})$ and so on.

Let me finish by mentioning that Kelley-Morse set theory is able to prove open determinacy for proper class games in much the same manner as we proved the Gale-Stewart theorem above, using well-ordered class meta-ordinals, rather than merely set ordinals, as well as in other ways. If there is interest, I can make a further post about that, so just ask in the comments!

Kelley-Morse set theory implies Con(ZFC) and much more

I should like to give a brief account of the argument that KM implies Con(ZFC) and much more. This argument is well-known classically, but unfortunately seems not to be covered in several of the common set-theoretic texts.

First, without giving a full formal axiomatization, let us review a little what KM is.  (And please see Victoria Gitman’s post on variant axiomatizations of KM.)  In contrast to Zermelo-Frankael (ZFC) set theory, which has a purely first-order axiomatization, both Kelley-Morse (KM) set theory and Gödel-Bernays (GBC) set theory are formalized in the second-order language of set theory, where we have two sorts of objects, namely sets and classes, in addition to the usual set membership relation $\in$. A model of KM will have the form $\langle M,{\in^M},S\rangle$, where $M$ is the collection of sets in the model, and $S$ is a collection of classes in the model; each class $A\in S$ is simply the subset of $M$.  Both KM and GBC will imply that $\langle M,{\in^M}\rangle$ is a model of ZFC.  Both GBC and KM assert the global choice principle, which asserts that there is a class that is a well-ordering of all the sets (or equivalently that there is a class bijection of all the sets with the class of ordinals). Beyond this, both GBC and KM have a class comprehension principle, asserting that for certain formulas $\varphi$, having finitely many set and class parameters, that $\{x \mid \varphi(x)\}$ forms a class. In the case of GBC, we have this axiom only for $\varphi$ having only set quantifiers, but in KM we also allow formulas $\varphi$ that have quantification over classes (which are interpreted in the model by quanfying over $S$). Both theories also assert that the intersection of a class with a set is a set (which amounts to the separation axiom, and this follows from replacement anyway).  In addition, both GBC and KM have a replacement axiom, asserting that if $u$ is a set, and for every $a\in u$ there is a unique set $b$ for which $\varphi(a,b)$, where $\varphi$ has finitely many class and set parameters, then $\{ b\mid \exists a\in u\, \varphi(a,b)\}$ is a set. In the case of GBC, we have the replacement axiom only when all the quantifiers of $\varphi$ are first-order quantifiers only, quantifying only over sets, but in KM we allow $\varphi$ to have second-order quantifiers.  Thus, both GBC and KM can be thought of as rather direct extensions of ZFC to the second-order class context, but KM goes a bit further by applying the ZFC axioms also in the case of the new second-order properties that become available in that context, while GBC does not.

The theorem I want to discuss is:

Theorem. KM proves Con(ZFC).

Indeed, ultimately we’ll show in KM that there is transitive model of ZFC, and furthermore that the universe $V$ is the union of an elementary chain of elementary rank initial segments $V_\theta\prec V$, each of which, in particular, is a transitive model of ZFC.

We’ll prove it in several steps, which will ultimately reveal stronger results and a general coherent method and idea.

KM has a truth predicate for first-order truth. The first step is to argue in KM that there is a truth predicate Tr for first-order truth, a class of pairs $(\varphi,a)$, where $\varphi$ is a first-order formula in the language of set theory and $a$ is an assignment of the free variabes of $\varphi$ to particular sets, such that the class Tr gets the right answer on the quantifier-free formulas and obeys the recursive Tarskian truth conditions for Boolean combinations and first-order quantification, that is, the conditions explaining how the truth of a formula is determined from the truth of its immediate subformulas.

To construct the truth predicate, begin with the observation that we may easily define, even in ZFC, a truth predicate for quantifier-free truth, and indeed, even first-order $\Sigma_n$ truth is $\Sigma_n$-definable, for any meta-theoretic natural number $n$. In KM, we may consider the set of natural numbers $n$ for which there is a partial truth predicate $T$, one which is defined only for first-order formulas of complexity at most $\Sigma_n$, but which gives the correct answers on the quantifier-free formulas and which obeys the Tarskian conditions up to complexity $\Sigma_n$.  The set of such $n$ exists, by the separation axiom of KM, since we can define it by a property in the second-order language (this would not work in GBC, since there is a second-order quantifier asking for the existence of the partial truth predicate).  But now we simply observe that the set contains $n=0$, and if it contains $n$, then it contains $n+1$, since from any $\Sigma_n$ partial truth predicate we can define one for $\Sigma_{n+1}$. So by induction, we must have such truth predicates for all natural numbers $n$.  This inductive argument really used the power of KM, and cannot in general be carried out in GBC or in ZFC.

A similar argument shows by induction that all these truth predicates must agree with one another, since there can be no least complexity stage where they disagree, as the truth values at that stage are completely determined via the Tarski truth conditions from the earlier stage.  So in KM, we have a unique truth predicate defined on all first-order assertions, which has the correct truth values for quantifier-free truth and which obeys the Tarskian truth conditions.

The truth predicate Tr agrees with actual truth on any particular assertion. Since the truth predicate Tr agrees with the actual truth of quantifier-free assertions and obeys the Tarskian truth conditions, it follows by induction in the meta-theory (and so this is a scheme of assertions) that the truth predicate that we have constructed agrees with actual truth for any meta-theoretically finite assertion.

The truth predicate Tr thinks that all the ZFC axioms are all true.  Here, we refer not just to the truth of actual ZFC axioms (which Tr asserts as true by the previous paragraph), but to the possibly nonstandard formulas that exist inside our KM universe. We claim nevertheless that all such formulas the correspond to an axiom of ZFC are still decreed true by the predicate Tr.  We get all the easy axioms by the previous paragraph, since those axioms are true under KM.  It remains only to verify that Tr asserts as true all instances of the replacement axiom. For this, suppose that there is a set $u$, such that Tr thinks every $a\in u$ has a unique $b$ for which Tr thinks $\varphi(a,b)$.  But now by KM (actually we need only GB here), we may apply the replacement axiom with Tr a predicate, to find that $\{ b\mid \exists a\in u\, \text{Tr thinks that} \varphi(a,b)\}$ is a set, whether or not $\varphi$ is an actual finite length formula in the metatheory. It follows that Tr will assert this instance of replacement, and so Tr will decree all instances of replacement as being true.

KM produces a closed unbounded tower of transitive models of ZFC. This is the semantic approach, which realizes the universe as the union of an elementary chain of elementary substructures $V_\theta$. Namely, by the reflection theorem, there is a closed unbounded class of ordinals $\theta$ such that $\langle V_\theta,{\in},\text{Tr}\cap V_\theta\rangle\prec_{\Sigma_1}\langle V,{\in},\text{Tr}\rangle$.  (We could have used $\Sigma_2$ or $\Sigma_{17}$ here just as well.)  It follows that $\text{Tr}\cap V_\theta$ fulfills the Tarskian truth conditions on the structure $\langle V_\theta,\in\rangle$, and therefore agrees with the satisfaction in that structure.  It follows that $V_\theta\prec V$ for first-order truth, and since ZFC was part of what is asserted by Tr, we have produced here a transitive model of ZFC. More than this, what we have is a closed unbounded class of ordinals $\theta$, which form an elementary chain $$V_{\theta_0}\prec V_{\theta_1}\prec\cdots\prec V_\lambda\prec\cdots,$$ whose union is the entire universe.  Each set in this chain is a transitive model of ZFC and much more.

An alternative syntactic approach. We could alternatively have reasoned directly with the truth predicate as follows.  First, the truth predicate is complete, and contains no contradictions, simply because part of the Tarskian truth conditions are that $\neg\varphi$ is true according to Tr if and only if $\varphi$ is not true according to Tr, and this prevents explicit contradictions from ever becoming true in Tr, while also ensuring completeness.  Secondly, the truth predicate is closed under deduction, by a simple induction on the length of the proof.  One must verify that certain logical validities are decreed true by Tr, and then it follows easily from the truth conditions that Tr is closed under modus ponens. The conclusion is that the theory asserted by Tr contains ZFC and is consistent, so Con(ZFC) holds. Even though Tr is a proper class, the set of sentences it thinks are true is a complete consistent extension of ZFC, and so Con(ZFC) holds.  QED

The argument already shows much more than merely Con(ZFC), for we have produced a proper class length elementary tower of transitive models of ZFC.  But it generalizes even further, for example, by accommodating class parameters.  For any class $A$, we can construct in the same way a truth predicate $\text{Tr}_A$ for truth in the first-order language of set theory augmented with a predicate for the class $A$.

In particular, KM proves that there is a truth predicate for truth-about-truth, that is, for truth-about-Tr, and for truth-about-truth-about-truth, and so on, iterating quite a long way. (Of course, this was also clear directly from the elementary tower of transitive models.)

The elementary tower of transitive elementary rank initial segments $V_\theta\prec V$ surely addresses what is often seen as an irritating limitation of the usual reflection theorem in ZFC, that one gets only $\Sigma_n$-reflection $V_\theta\prec_{\Sigma_n} V$ rather than this kind of full reflection, which is what one really wants in a reflection theorem.  The point is that in KM we are able to refer to our first-order truth predicate Tr and overcome that restriction.

Doesn’t the existence of a truth predicate violate Tarski’s theorem on the non-definability of truth?  No, not here, since the truth predicate Tr is not definable in the first-order language of set theory. Tarski’s theorem asserts that there can be no definable class (even definable with set parameters) that agrees with actual truth on quantifier-free assertions and which satisfies the recursive Tarskian truth conditions.  But nothing prevents having some non-definable class that is such a truth predicate, and that is our situation here in KM.

Although the arguments here show that KM is strictly stronger than ZFC in consistency strength, it is not really very much stronger, since if $\kappa$ is an inaccessible cardinal, then it is not difficult to argue in ZFC that $\langle V_\kappa,\in,V_{\kappa+1}\rangle$ is a model of KM. Indeed, there will be many smaller models of KM, and so the consistency strength of KM lies strictly between that of ZFC, above much of the iterated consistency hierarchy, but below that of ZFC plus an inaccessible cardinal.