Recursively saturated and rather classless

A mathematics blog by Kameryn Williams

Killing truth

It is not difficult to construct models of \mathsf{ZFC} whose truth predicate is not strongly amenable, where X \subseteq M is strongly amenable if the structure (M,X) satisfies the Collection and Separation schemata in the expanded language. Namely, this can be accomplished by considering a pointwise definable model of \mathsf{ZFC}, such as the Shepherdson–Cohen least transitive model. The truth predicate for the model M reveals that it is countable, allowing one to define a surjection \omega^M \to M. This witnesses a failure of Replacement (in the expanded language).

On the other hand, one can find models whose truth predicate is strongly amenable. If (M,\mathcal X) \models \mathsf{GBC} contains the truth predicate for M then its truth predicate must be strongly amenable, due to the Class Replacement and Class Comprehension axioms of \mathsf{GBC}. In particular, if (M,\mathcal X) satisfies Kelley–Morse set theory (or any other second-order set theory which proves the existence of the truth predicate) then truth will be strongly amenable for M.

Let’s consider those models whose truth is strongly amenable. If we have a \mathsf{GBC}-realization for such a model can we always add more classes  (but not sets!) to expand it to a \mathsf{GBC} model which contains the truth predicate?

The answer is no. For countable models we can kill truth with the right \mathsf{GBC}-realization, so that no matter what new classes we add we cannot have the truth predicate without violating Class Replacement.

Proposition: Let M \models \mathsf{ZFC} be a countable \omega-model. Then there is a \mathsf{GBC}-realization \mathcal X \subseteq \mathcal P(M)  for M so that no \mathsf{GBC}-realization \mathcal Y \supseteq \mathcal X can contain the truth predicate for M.

The purpose of requiring M to have a well-founded \omega is the Krajewski phenomenon that countable \omega-nonstandard models of set theory which admit ‘truth predicates’ which measure the truth of all—internal, possibly nonstandard—formulae (full satisfaction classes, to use the jargon) admit continuum many different ones. So in such case there is not a unique object to kill off (indeed, it’s not sensible to speak of the truth predicate for M in the absence of an already-fixed second-order part) and the situation becomes much trickier.

But more on that later. Let’s see why this proposition is true.

Proof: Suppose that truth is strongly amenable for M. Otherwise, no \mathsf{GBC}-realization for M can contain the truth predicate and there is nothing to prove. We will produce the desired \mathcal X by adding a carefully constructed Cohen-generic subclass of \mathrm{Ord}. Let \mathbb C be this class forcing, i.e. the partially ordered class consisting of set-sized partial functions \mathrm{Ord} \to 2, ordered by reverse inclusion. This forcing is \kappa-closed and \kappa-distributive for every cardinal \kappa so it does not add new sets.

Claim: There is a sequence \langle D_i : i \in \mathrm{Ord} \rangle of definable dense subclasses of \mathbb C which is (1) definable from the truth predicate for M and (2) meeting every D_i is sufficient to guarantee a filter is generic over M.

It is clear that the collection of dense subclasses of \mathbb C is definable from the truth predicate; the truth predicate allows one to see whether \varphi(x,a) defines a dense subclass of \mathbb C and so the whole collection can be indexed by (\varphi, a). The trick is to extract a sequence of ordertype \mathrm{Ord}. This is trivial if M has a definable global well-order, but in general this may not be true. In such case, use that \mathbb C is \kappa-distributive for every \kappa. So given a set-sized collection of dense subclasses we can find a single dense subclass below all of them. So we get the D_is as in the claim by taking D_i to be below all dense subclasses definable from parameters in V_i.

We will now use this \langle D_i : i \in \mathrm{Ord} \rangle to define a Cohen-generic subclass C of \mathrm{Ord}. Externally to the model, fix an \omega-sequence cofinal in \mathrm{Ord}^M. Think of this sequence as an \mathrm{Ord}^M-length binary sequence \langle b_i : i \in \mathrm{Ord} \rangle, consisting mostly of zeros with the rare one. This sequence is amenable over M, since its initial segments have only finitely many ones. On the other hand, it is not strongly amenable since from this sequence can be defined a cofinal map \omega \to \mathrm{Ord}, contradicting an instance of Replacement.

We build C in \mathrm{Ord}^M steps. Start with c_0 = \emptyset. Given c_i let c_{i+1}' = c_i {}^\smallfrown \langle b_i \rangle and then extend c_{i+1}' to c_{i+1} meeting D_i, where we require the extension to be minimal in length to meet D_i. (If there is more than one way to meet D_i of minimal length, choose between them arbitrarily.) At limit stages take unions of the previous stages. Finally, set C = \bigcup_{i \in \mathrm{Ord}} c_i. Then C is generic over M since it meets every D_i. But hidden within C is this bad sequence \langle b_i \rangle.

I claim now that from both C and the truth predicate for M one can define \langle b_i \rangle. This is done inductively. We know b_0 because it is the first bit of C. From the truth predicate we know the minimal amount we have to extend \langle b_0 \rangle in order to meet D_0, because the sequence \langle D_i \rangle is definable from the truth predicate. So we can recover c_1. We now repeat this process, discovering b_2 as the first bit of C after c_1 and thereby can define c_2 by knowing the minimal length we had to extend to meet D_2. And so on we define b_i and c_i for all i \in \mathrm{Ord}^M. So if we have access to both C and the truth predicate then we can define the sequence \langle b_i \rangle.

But if we can define the bad sequence then our model must fail to satisfy Class Replacement. Thus, there can be no \mathsf{GBC}-realization for $M$ which contains both C and the truth predicate for M. So \mathrm{Def}(M;C) is a \mathsf{GBC}-realization for M which cannot be extended to a \mathsf{GBC}-realization which contains the truth predicate, as desired. (To see (M,\mathrm{Def}(M;C)) \models \mathsf{GBC} observe that every Cohen-generic subclass of \mathrm{Ord} codes a global well-order by comparing where each set is first coded into the generic.) ∎

As mentioned above, Kelley–Morse proves the existence of the truth predicate for the first-order part, as do many much weaker theories. As a consequence we get \mathsf{GBC} models which cannot be expanded by adding classes to get a model of \mathsf{KM}, even if the first-order part has some other \mathsf{KM}-realization.

Corollary: Let M \models \mathsf{ZFC} be any countable \omega-model. Then M has a \mathsf{GBC}-realization which cannot be extended to a \mathsf{KM}-realization. The same is true if \mathsf{KM} is replaced by \mathsf{GBC} plus Elementary Transfinite Recursion, or even \mathsf{GBC} + \mathsf{ETR}_\omega.

What this result suggest is that it matters how one builds up one’s classes. It is not difficult to see that, say, \mathsf{KM} proves there exist classes of ordinals which are Cohen-generic over the definable classes. (The truth predicate lets us list the definable dense subclasses of the forcing, so they can be met one at a time.) So if we want to build up a model of \mathsf{KM} from a fixed universe of sets we must add Cohen-generics at some point. The above shows that it matters which generics we pick. One wrong step along the way and we stumble off the narrow path leading to paradise.

Observe that the proposition relativizes. Fixing a possible class X \subseteq M if X can be put in any \mathsf{GBC}-realization for M then there is a \mathsf{GBC}-realization for M containing X which cannot be extended to one containing the truth predicate relative to the parameter X. As a consequence, one can find \mathsf{GBC}-realizations for any strong enough countable \omega-model M which contain an iterated truth predicate of length \Gamma but which cannot be extended to a \mathsf{GBC}-realization containing an iterated truth prediacte of length \Gamma + 1.

As a coda, let me return \omega-nonstandard models. Here, things go badly. As mentioned earlier, Krajewski showed that if a countable \omega-nonstandard model of set theory admits a ‘truth predicate’ (full satisfaction class) then it admits continuum many different ones. So killing off one possible truth predicate will not immediately ensure that the classes cannot be expanded to include truth; perhaps some other full satisfaction class can be added to the classes to be truth. But a version of the above argument does show that we can kill off individual full satisfaction classes. (A strongly amenable full satisfaction class will tell us about dense subclasses of the Cohen-forcing which are ‘defined’ using a nonstandard formula, but it will also tell us about all the really definable dense subclasses, so it is good enough.) Can we kill off all the full satisfaction classes? I don’t (yet?) know!

Question: If M \models \mathsf{ZFC} is countable and \omega-nonstandard must it be the case that there is a \mathsf{GBC}-realization \mathcal X for M so that no matter how we expand \mathcal X we never get \mathcal Y so that (M,\mathcal Y) satisfies \mathsf{GBC} plus “there is a truth predicate for first-order truth”?

 

Advertisements

The length of inductive iterated full satisfaction classes

This will be a talk at the CUNY Models of Peano Arithmetic seminar on Wednesday, October 25.

Last week, I gave an application—due to Krajewski—of iterated full satisfaction classes. As part of that we saw that if M \models \mathsf{PA} is resplendent then M admits an iterated full satisfaction class of any length. But in general, these need not be inductive, as even a fragment of induction in the language with the satisfaction class is enough to prove \mathrm{Con}(\mathsf{PA}). This week, we will consider inductive iterated full satisfaction classes.

It is clear that if a resplendent model satisfies the right theory then it admits an inductive iterated full satisfaction class of length n. But that does not imply than any given inductive iterated full satisfaction class of length < n over the model can be extended to one of length n. This is the main result I will talk about: there are models of arithmetic which admit inductive iterated full satisfaction classes S,S' of length n where S can be extended to an inductive iterated full satisfaction class of length n+1 while S' cannot. A slight strengthening of this result will let us draw conclusions about the tree of inductive iterated full satisfaction classes over, say, countable models of arithmetic. Namely, under appropriate hypotheses, for each levels n \le m in the tree there are continuum many nodes on level n in the tree which can be extended to level m but no further.

Chains and antichains of finitely axiomatizable theories conservative over Peano arithmetic

This will be a talk at the CUNY Models of Peano Arithmetic Seminar on Wednesday, October 18.

It is well-known that there are finitely axiomatizable theories which are conservative over Peano arithmetic. Perhaps the best known of these is \mathsf{ACA}_0, the third of the “big five” subsystems of second-order arithmetic from reverse mathematics. Other examples of such theories come from the addition of satisfaction classes, as a consequence of a famous result by Kotlarski, Krajewski, and Lachlan. In unpublished work, Krajewski extended these ideas to construct chains and antichains of finitely axiomatizable theories conservative over \mathsf{PA}. I will present his results. Namely, I will show (1) that there are length \omega ascending and descending \subseteq-chains of finitely axiomatizable theories conservative over \mathsf{PA}. We will also get chains of such theories of order \mathbb Q. I will additionally show (2) that there are countable \subseteq-antichains of finitely axiomatizable theories conservative over \mathsf{PA}.

Strong second-order set theories do not have least transitive models

This will be a talk at the University of Pennsylvania Logic and Computation Seminar on Monday, November 13. See also their page for the talk. Slides available here.

Shepherdson and Cohen independently showed that (if there is any transitive model of \mathsf{ZFC}) there is a least transitive model of \mathsf{ZFC}. That is, there is a transitive set M so that (M,\in) \models \mathsf{ZFC} and if N is any transitive model of \mathsf{ZFC} then M \subseteq N. We can ask the same question for theories extending \mathsf{ZFC}. For some fixed set theory T, does T have a least transitive model?

I will look at this question where T is a second-order set theory.  Two major second-order set theories of interest are Gödel–Bernays set theory \mathsf{GBC} and Kelley–Morse set theory \mathsf{KM}. The weaker of the two is \mathsf{GBC}, which is conservative over \mathsf{ZFC} while \mathsf{KM} is much stronger.

As an immediate corollary of the Shepherdson–Cohen result we get that there is a least transitive model of \mathsf{GBC}. The case for \mathsf{KM} is more difficult and indeed, has a negative answer. I will show that there is no least transitive model of \mathsf{KM}. Along the way we will build Gödel’s constructible universe above sets and into the proper classes, unroll models of second-order set theory into first-order models, and dip our toes into Barwise theory and the admissible cover. Time permitting I will mention some results and open questions about \mathsf{GBC} + Elementary Transfinite Recursion, which is intermediate between \mathsf{GBC} and \mathsf{KM} in strength.

friedman-things

The exact strength of the class forcing theorem

This will be a talk at CUNY Set Theory Seminar on Friday, October 13.

Slides.

Gödel–Bernays set theory \mathsf{GBC} proves that sufficiently nice (i.e. pretame) class forcings satisfy the forcing theorem—that is, these forcing relations \mathbb P admit forcing relations \Vdash_\mathbb{P} satisfying the recursive definition of the forcing relation. It follows that statements true in the corresponding forcing extensions are forced and forced statements are true. But there are class forcings for which having their forcing relation exceeds \mathsf{GBC} in consistency strength. So \mathsf{GBC} does not prove the forcing theorem for all class forcings. This is in contrast to the well-known case of set forcing, where \mathsf{ZFC} proves the forcing theorem for all set forcings. On the other hand, stronger second-order set theories such as Kelley–Morse set theory \mathsf{KM} prove the forcing theorem for all class forcings, providing an upper bound. What is the exact strength of the class forcing theorem?

I will show that, over \mathsf{GBC}, the forcing theorem for all class forcings is equivalent to \mathsf{ETR}_\mathrm{Ord} the principle of elementary transfinite recursion for recursions of height \mathrm{Ord}. This is equivalent to the existence of \mathrm{Ord}-iterated truth predicates for first-order truth relative to any class parameter; which is in turn equivalent to the existence of truth predicates for the infinitary languages \mathcal L_{\mathrm{Ord}, \omega}(\in, A) allowing any class parameter A. This situates the class forcing theorem precisely in the hierarchy of theories between \mathsf{GBC} and \mathsf{KM}.

This is joint work with Victoria Gitman, Joel Hamkins, Peter Holy, and Philipp Schlict from our paper of the same name.

ClassForcing

The exact strength of the class forcing theorem

This will be a talk at the Kurt Gödel Research Center Research Seminar on Tuesday, September 26. See also their page for the talk. Slides here.

Gödel–Bernays set theory \mathsf{GBC} proves that sufficiently nice (i.e. pretame) class forcings satisfy the forcing theorem—that is, these forcing relations \mathbb P admit forcing relations \Vdash_\mathbb{P} satisfying the recursive definition of the forcing relation. It follows that statements true in the corresponding forcing extensions are forced and forced statements are true. But there are class forcings for which having their forcing relation exceeds \mathsf{GBC} in consistency strength. So \mathsf{GBC} does not prove the forcing theorem for all class forcings. This is in contrast to the well-known case of set forcing, where \mathsf{ZFC} proves the forcing theorem for all set forcings. On the other hand, stronger second-order set theories such as Kelley–Morse set theory \mathsf{KM} prove the forcing theorem for all class forcings, providing an upper bound. What is the exact strength of the class forcing theorem?

I will show that, over \mathsf{GBC}, the forcing theorem for all class forcings is equivalent to \mathsf{ETR}_\mathrm{Ord} the principle of elementary transfinite recursion for recursions of height \mathrm{Ord}. This is equivalent to the existence of \mathrm{Ord}-iterated truth predicates for first-order truth relative to any class parameter; which is in turn equivalent to the existence of truth predicates for the infinitary languages \mathcal L_{\mathrm{Ord}, \omega}(\in, A) allowing any class parameter A. This situates the class forcing theorem precisely in the hierarchy of theories between \mathsf{GBC} and \mathsf{KM}.

This is joint work with Victoria Gitman, Joel Hamkins, Peter Holy, and Philipp Schlict from our paper of the same name.

ClassForcing

On the length of iterated full satisfaction classes

This will be a talk at the Warsaw Workshop on Formal Truth Theories on 2017 Sept 29.

In second-order arithmetic, the principle of arithmetical transfinite recursion \mathsf{ATR} asserts that every arithmetical recursive definition iterated transfinitely has a solution. One particular recursive definition of interest is Tarski’s definition of a truth predicate. This definition is carried out over a well-founded tree of rank \omega. We can go further, defining truth about truth via an arithmetical recursion of rank \omega + \omega, truth about truth about truth via an arithmetical recursion of rank \omega \cdot 3, and so on. In general, \mathsf{ATR} implies the existence of an iterated truth predicate of length \alpha for any ordinal \alpha, by way of a recursion over a tree of rank \omega \cdot \alpha.

Consider now a nonstandard model (M,\mathcal X) of \mathsf{ATR}_0 (= \mathsf{ACA}_0 + \mathsf{ATR}). Since M is nonstandard \mathcal X cannot contain the real truth predicate for M, as from it (M,\mathcal X) could define the standard cut of M. Instead, the object which (M,\mathcal X) thinks is the truth predicate for M is an inductive full satisfaction class. This full satisfaction class is not confined to the real formulae as seen from outside, but also decides the truth or falsity of all formulae (in M) of nonstandard length. More generally, for any \Gamma \in \mathcal X which (M,\mathcal X) thinks is a well-order, \mathcal X contains an inductive \Gamma-iterated full satisfaction class.

(M,\mathcal X) thinks that its full satisfaction class is {\em the} unique truth predicate for M. Given two would-be truth predicates (M,\mathcal X) can inductively show that they agree at each level and thus are the same. Similarly, (M,\mathcal X) thinks its \Gamma-iterated full satisfaction class is the unique \Gamma-iterated truth predicate.

Externally to (M,\mathcal X), however, we know that full satisfaction classes, not even inductive full satisfaction classes, have to be unique. Indeed, as Krajewski showed, no countable (nonstandard) M has a unique inductive full satisfaction class. Analogous questions can be asked about iterated full satisfaction classes. It is easy to see they will not be unique for countable models; if S is an inductive full satisfaction class for countable M then a version of Krajewski’s proof applies to (M,S) to show that M admits continuum many 2-iterated full satisfaction classes which extend S. (With some mild assumptions on M and S we can get continuum many inductive 2-iterated full satisfaction classes extending S.)

Uniqueness is out of the question, but we might hope some invariant can be found. If S is an inductive full satisfaction class for M, we can possibly extend it to an inductive 2-iterated full satisfaction class, then an inductive 3-iterated full satisfaction class, and so on until we reach a point that the iterated full satisfaction class is no longer inductive. If S and S' are inductive full satisfaction classes for M, is the length we can iterate them the same? For that matter, is this length well-defined?

The answer to both questions is no.

Theorem: Suppose that countable nonstandard M \models \mathsf{PA} satisfies the \mathcal L_{\mathsf{PA}}-consequences of \mathsf{PA} + “there is an inductive 2-iterated truth predicate”. If M admits an inductive full satisfaction class, then there are S and S' inductive full satisfaction classes for M so that S can be iterated one step further to get an inductive 2-iterated full satisfaction class while S' cannot.

More generally, the iteration length can be anything at all.

Consider countable nonstandard M \models \mathsf{PA} and a < b \in M. Suppose that M satisfies the \mathcal L_\mathsf{PA}-consequences of \mathsf{PA} + “there is an inductive b-iterated truth predicate”. Then, if M admits an inductive a-iterated truth predicate, there are S_a and S_a' inductive a-iterated full satisfaction classes for M so that S_a can be iterated one step further to an inductive (a+1)-iterated full satisfaction class while S_a' cannot.

My original motivation for investigating these questions was in the context of models of set theory, where similar results apply. Suppose M \models \mathsf{ZF} is countable and \omega-nonstandard and satisfies the \mathcal L_\mathsf{ZF}-consequences of \mathsf{ZF} + “there is a strongly amenable 2-iterated truth predicate”. (Being strongly amenable is the set theoretic analogue of being inductive.) Then, if M admits a strongly amenable full satisfaction class, there are S and S' strongly amenable full satisfaction classes for M so that S can be extended to a strongly amenable 2-iterated full satisfaction class while S' cannot. Similar to the arithmetic case, this generalizes to longer iteration lengths.

As a consequence of this, plus the fact that having solutions to any transfinite recursion is equivalent to having solutions for the recursions to construct iterated truth predicates, strongly separating weak fragments of \mathsf{ETR} is only possible with \omega-standard models. Here, \mathsf{ETR} (Elementary Transfinite Recursion) is a set theoretic analogue of \mathsf{ATR}, introduced by Fujimoto. Say that M \models \mathsf{ZF} strongly separates second-order set theories T and S if M satisfies the first-order consequences of S and of T and there is \mathcal T \subseteq \mathcal P(M) so that (M,\mathcal T) \models T but no \mathcal S \subseteq \mathcal P(M) so that (M,\mathcal S) \models S. Intuitively, M strongly separates S and T if M can be made a model of S but cannot be made a model of T, and this is due to something inherently second-order rather than due to some first-order property of M.

For an ordinal \alpha, let \mathsf{ETR}_\alpha denote the principle that elementary transfinite recursions of rank \le \alpha have solutions. If \beta \gg \alpha then \mathsf{ETR}_\beta and \mathsf{ETR}_\alpha can be separated, simply because \mathsf{ETR}_\beta implies \mathrm{Con}(\mathsf{ETR}_\alpha) (over Gödel–Bernays set theory). This separation can be witnessed by an \omega-nonstandard model. However, if countable M strongly separates \mathsf{ETR}_\beta and \mathsf{ETR}_\alpha then M must be \omega-standard. Indeed, \mathsf{ETR}_\beta and \mathsf{ETR}_\alpha are strongly separated by a transitive model of \mathsf{ZF}.

No such phenomenon occurs in arithmetic, as there is only one standard model of arithmetic. We cannot strongly separate the existence of iterated truth predicates of different length with countable models.