Towsner's stable forcing
It is well known that a model of satisfies induction () if and only if it satisfies bounded comprehension: if is a formula (with parameters) then the set exists for every number in . Thus, it follows that induction also holds and indeed induction holds for all boolean combinations of formulas. However, offers no control over sets of higher complexity than that. In particular, induction may fail very badly in a model of . Indeed, by a result of Slaman (2004) induction is equivalent to bounding () and it is known that we have a strict hierarchy:
The actual size of the gaps between and has recently been quantified by Towsner (2015), who used a beautiful forcing argument to show that gives absolutely no control whatsoever on definable sets.
Theorem (Towsner 2015). If is a model of and is any external set of numbers in then there is an extension of that satisfies and such that is definable in .
Theorem (Towsner 2015). If is a model of and is any external set of numbers in then there is an extension of that satisfies and such that is definable in .
I will only outline the proof of the first result. The Limit Lemma gives a very combinatorial way to understand definable sets over . Namely, the external set is definable in exactly when there is a function in such that exists for every and . In general, a function such that exists for every is called stable. Towsner’s strategy is to generically add a stable coloring such that and show that the forcing to add such a coloring preserves .
Towsner doesn’t name this forcing, so I will take the liberty of coining a name for it — Towsner’s Stable Forcing and I will denote it — at least for the purpose of this post. The forcing can be described as follows. Conditions of are pairs where is (a code for) an finite partial function and is a truly finite set of stability promises (discussed shortly); and the ordering of conditions is iff extends and . The stability promises consist of pairs that promise that the values of the generic coloring with first coordinate stabilize from on to the correct value predicted by . More precisely, if then , , and for all such that . Since is not in and usually has no way of distinguishing truly finite sets from others, the forcing is not definable in though all conditions are in . It is therefore hopeless try to internalize this forcing but we will see that if is a (sufficiently) generic filter over , then defines a total coloring and that is as required for the theorem.
The main difficulty is in showing that still satisfies . The trick is that if an extension forces a bounded statement, then only an finite amount of the information of the information that knows about is actually used to witness that fact. Though contains an infinite amount of promised information, we can trim down and throw all the information actually used into to get a new condition that still forces the bounded statement and has no more stability promises than had. Thus, if where is bounded, then there are an extension with and such that . Using this, given a condition and a formula we can work in to find an extension with such that Since , we know that actual condition in , provided that is one in the first place, without worrying about , true finiteness, or anything that is not within reach of .
Of course, this forcing construction is only a small part of Towsner’s excellent paper, I highly recommend reading it!
References

T. A. Slaman, 2004: $\Sigma_n$bounding and $\Delta_n$induction, Proc. Amer. Math. Soc. 132, no. 8, 2449–2456.

mr: 2052424

zbl: 1053.03034


H. Towsner, 2015: On maximum conservative extensions, Computability 4, no. 1, 57–68.

mr: 3373217

zbl: 1326.03072

arxiv: 1302.1488

doi: 10.3233/COM150033

Originally posted on by François G. Dorais. To the extent possible under law, François G. Dorais has waived all copyright and neigboring rights to this work.
Comments

François G. Dorais wrote
Edit: I redacted a claim that the second result follows from the first using arguments similar to those Jared Corduan and I used in _On the indecomposability of _. That unfortunate claim was at best incomplete and possibly false. Since the claim was only tangential to the topic, early redaction was the best course of action.

Peter Krautzberger wrote
Excellent piece of research blogging. You could generate a citation via mathblogging.org and add it.

François G. Dorais replied to Peter Krautzberger
How does one generate a citation?

Peter Krautzberger replied to François G. Dorais
Got to Mathblogging.org, hit the menu item “Generate Citation”, follow instructions?

François G. Dorais replied to Peter Krautzberger
The citations are MLA style, which I am not particularly fond of, and WordPress tends to strip some stuff out. What parts are necessary to make scanning work?

Peter Krautzberger replied to François G. Dorais
I’m not sure, but I’m guessing the titletag of the span is the only crucial thing since it contains structured data.