Is set-induction relatively consistent? - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-23T05:10:20Z http://mathoverflow.net/feeds/question/12754 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/12754/is-set-induction-relatively-consistent Is set-induction relatively consistent? Mike Shulman 2010-01-23T17:41:08Z 2010-06-13T23:13:44Z <p>One way to state the <a href="http://en.wikipedia.org/wiki/Axiom%5Fof%5Ffoundation" rel="nofollow">axiom of foundation</a> is that the $\in$ relation on any <a href="http://en.wikipedia.org/wiki/Transitive%5Fset" rel="nofollow">transitive set</a> is <em>well-founded</em> in the following sense:</p> <ul> <li>A relation $(X,\prec)$ is well-founded if for any subset $S\subseteq X$ which is <em>inductive</em>, in the sense that $y\in S$ for all $y\prec x$ implies $x\in S$, in fact $S=X$.</li> </ul> <p>This is classically equivalent to the <a href="http://en.wikipedia.org/wiki/Well-founded%5Frelation" rel="nofollow">more usual</a> definition, but constructively more reasonable. Now in constructive set theories such as <a href="http://en.wikipedia.org/wiki/Constructive%5Fset%5Ftheory#Aczel.27s%5Fconstructive%5FZermelo-Fraenkel" rel="nofollow">CZF</a>, one often finds a different axiom of "foundation" called <em>set-induction</em> or <a href="http://en.wikipedia.org/wiki/Epsilon-induction" rel="nofollow">epsilon-induction</a>:</p> <ul> <li>For any formula $\phi$, if $\phi(x)$ for all $x\in y$ implies $\phi(y)$ for any set $y$, then in fact $\phi(x)$ is true for all sets $x$.</li> </ul> <p>This certainly implies that $\in$ is well-founded on any transitive set in the sense above, and the converse is true <em>if</em> every set has a transitive closure and you have the full axiom of separation, since from any transitive set $x$ you can form $\lbrace y\in x \mid \phi(y) \rbrace$ and conclude that it is all of $x$.</p> <p>Now classically, one can show that the axiom of foundation is consistent, relative to the other axioms of set theory, by simply restricting any model to the submodel of well-founded sets. I <em>think</em> you can do this in CZF for the version of "foundation" I stated above, that every transitive set is well-founded. My question is, can you do anything similar with set-induction? I care most about CZF, but I'd also be interested to know about results in any other theory lacking the full axiom of separation.</p> <p>(BTW, it's possible one might have to fiddle a little bit with what I mean by "the other axioms of CZF" to make this nontrivial. For one thing, let's drop the axiom of infinity, since I see no guarantee that $\omega$ would be "strongly well-founded" in the necessary sense.)</p> http://mathoverflow.net/questions/12754/is-set-induction-relatively-consistent/13091#13091 Answer by Mike Shulman for Is set-induction relatively consistent? Mike Shulman 2010-01-27T02:29:29Z 2010-01-27T02:29:29Z <p>I think there shouldn't be a problem showing that the "strongly well-founded" or "class-well-founded" sets satisfy most of the basic axioms of set theory that involve only $\Delta_0$-quantifiers, e.g. pairs, unions, $\Delta_0$-separation. The problem should mainly be with the axioms like replacement and collection that involve unbounded quantifiers since "class-well-foundedness" isn't specified by a single formula so you can't just restrict the quantifiers to range over those sets. In fact, it's not even clear that the class-well-founded sets would satisfy set-induction, since the meaning of the quantifiers has changed.</p> <p>I found a partial answer to a related problem in Mathias' paper "The strength of Mac Lane set theory." In Prop. 6.39 he proves that in a metatheory with a strong enough axiom of separation ($\Sigma_1$), if we start with a model N of a certain weak theory including KP and $\Sigma_1$-foundation and whose natural numbers are actually well-founded (in the sense of the metatheory), then the submodel M of N consisting of those "sets" whose rank in N is actually well-founded forms a model of the same theory plus "class foundation" (= set-induction). As expected, the main difficulty is in proving $\Delta_0$-collection.</p> http://mathoverflow.net/questions/12754/is-set-induction-relatively-consistent/13096#13096 Answer by François G. Dorais for Is set-induction relatively consistent? François G. Dorais 2010-01-27T03:57:31Z 2010-06-08T14:42:45Z <p>Let KP<sup>0</sup> be the induction-free fragment of KP. That is, the axioms of KP<sup>0</sup> are extensionality, pairing, union, &Delta;<sub>0</sub>-separation, &Delta;<sub>0</sub>-collection, and (since I see no way of proving this from the other axioms) the existence of transitive closures.</p> <p>Following Barwise, I define the class of &Sigma;-formulas to be the smallest class which contains atomic formulas and their negations, and which is closed under conjunction, disjunction, bounded quantification, and unbounded existential quantification. Similarly, I define the of &Pi;-formulas to be the smallest class which contains atomic formulas and their negations, and which is closed under conjunction, disjunction, bounded quantification, and unbounded universal quantification. The negation of a &Sigma;-formula &phi; is canonically equivalent to a &Pi;-formula and vice versa; I will identify &not;&phi; with its canonical equivalent without further comment.</p> <p>The following three facts are standard in KP. The usual proofs actually go through in KP<sup>0</sup>.</p> <p><b>&Sigma;-Reflection.</b> For every &Sigma;-formula KP<sup>0</sup> &#8870; &phi; &harr; &exist;a&phi;<sup>(a)</sup>, where &phi;<sup>(a)</sup> is obtained from &phi; by replacing every unbounded quantifier &exist;x by the corresponding bounded quantifier &exist;x&isin;a.</p> <p><b>&Sigma;-Collection.</b> For every &Sigma;-formula &phi;(u,v), <p>KP<sup>0</sup> &#8870; &forall;u&isin;x&exist;v&phi;(u,v) &rarr;&exist;y&forall;u&isin;x&exist;v&isin;y&phi;(u,v).</p> <p><b>&Delta;-Separation.</b> For every &Sigma;-formula &phi;(u) and every &Pi;-formula &psi;(u),</p> <p>KP<sup>0</sup> &#8870; &forall;u&isin;x(&phi;(u) &harr; &psi;(u)) &rarr; &exist;y&forall;u&isin;x(u &isin; y &harr; &phi;(u)),</p> <p>where y does not occur free in &phi; nor &psi;.</p> <p>Instead of Mike Shulman's foundation axiom, I will use the classically equivalent regularity axiom:</p> <p>(Reg) x &ne; &empty; &rarr; &exist;y&isin;x(x&cap;y = &empty;).</p> <p>This axiom already implies a certain amount of induction because of &Delta;-separation.</p> <p><b>&Delta;-Induction.</b> For every &Sigma;-formula &phi;(u) and every &Pi;-formula &psi;(u),</p> <p>KP<sup>0</sup> + Reg &#8870; &forall;u(&phi;(u) &harr; &psi;(u)) &rarr; (&forall;u(&forall;v&isin;u&phi;(v) &rarr; &phi;(u)) &rarr; &forall;u&phi;(u)).</p> <p>For convenience, I will now assume that the language contains a function symbol rk(x) for the ordinal rank of a set. Let A be a model of KP<sup>0</sup> + Reg. A cut in A is a proper initial segment I of the ordinals of A which has no least upper bound; a &Sigma;-cut (resp. &Pi;-cut) is one which can be defined by a &Sigma;-formula (resp. &Pi;-formula).</p> <p><b>&Sigma;-Cut Lemma.</b> If A is a model of KP<sup>0</sup> + Reg and I is a &Sigma;-cut in A, then A<sub>I</sub> = {x &isin; A : rk(x) &isin; I} is a model of KP<sup>0</sup> + Reg.</p> <p><i>Sketch of proof.</i> The main point of contention is &Delta;<sub>0</sub>-collection. Suppose that &phi;(u,v) is a &Delta;<sub>0</sub>-formula such that A<sub>I</sub> &#8871; &forall;u&isin;x&exist;v&phi;(u,v). Consider the set of ordinals</p> <p>J = {&alpha; &isin; A : &exist;u&isin;x&forall;v(rk(v) &lt; &alpha; &rarr; &not;&phi;(u,v))}.</p> <p>This is a &Pi;-definable initial segment of I. We cannot have I = J, since that would violate &Delta;-induction. Pick &beta; &isin; I \ J. Working in A, we can find a set y such that</p> <p>&forall;u&isin;x&exist;v&isin;y(rk(v) &lt; &beta; &and; &phi;(u,v)).</p> <p>If necessary, we can cut down y so that rk(y) &le; &beta; and hence y &isin; A<sub>I</sub>. &#8718;</p> <p>If A has a minimal &Sigma;-cut, then this gives a model of KP<sup>0</sup> that satisfies &Sigma;-induction. Unfortunately, there are models of KP<sup>0</sup> + Reg without minimal &Sigma;-cut.</p> <p>Now, on the positive side a minor twist of the proof of the &Sigma;-cut lemma gives the following.</p> <p><b>&Pi;-Cut Lemma.</b> If A is a model of KP<sup>0</sup> that satisfies &Pi;-induction and I is any cut of A, then A<sub>I</sub> is a model of KP<sup>0</sup>.</p> <p>(&Pi;-induction implies that the &Pi; set J defined as above must have a least upper bound &beta; &isin; I. The rest of the proof is identical.)</p> <p>So when A satisfies &Pi;-induction, we can take a sufficiently small cut of A to get a model of KP (with full induction). In fact, we can take the maximal wellfounded initial segment of the ordinals of A, with the caveat that this cut is very often just &omega;.</p> <p>When I have a chance, I'll try to add examples showing that you can't do better than the &Sigma;-cut lemma and the &Pi;-cut lemma.</p> <hr> <p><strong>Addendum.</strong> I just stumbled across two papers that address these questions. The first paper is by Domenico Zambella <em>Foundation versus induction in Kripke-Platek set theory</em> [J. Symb. Logic 63 (1998), <a href="http://www.ams.org/mathscinet-getitem?mr=1665739" rel="nofollow">MR1665739</a>] where it is shown that foundation implies open-induction, but not &Sigma;<sub>1</sub>-induction over KP<sup>0</sup> (without transitive closures). This is complemented by Antonella Mancini and Domenico Zambella <em>A Note on Recursive Models of Set Theories</em> [Notre Dame J. Formal Logic 42 (2001), <a href="http://www.ams.org/mathscinet-getitem?mr=1993394" rel="nofollow">MR1993394</a>] where they generalize Tennenbaum's Theorem by showing that fragments of KP which prove &Sigma;<sub>1</sub>-induction have no computable models other than the standard one.</p> http://mathoverflow.net/questions/12754/is-set-induction-relatively-consistent/28072#28072 Answer by Daniel Mehkeri for Is set-induction relatively consistent? Daniel Mehkeri 2010-06-13T23:13:44Z 2010-06-13T23:13:44Z <p>Late answer: NO. At least with respect to CZF.</p> <p>CZF with Set Induction has proof-theoretic ordinal the Bachmann-Howard ordinal.</p> <p>CZF without Set Induction is weaker. Can't think of a direct reference, but:</p> <ul> <li>Crosilla &amp; Rathjen "Inaccessible Set Axioms may have little consistency strength" </li> </ul> <p>It is shown that CZF without set induction but with an inaccessible set axiom has proof-theoretic ordinal $\Gamma_0$. </p> <p>This is strictly less than the Bachmann-Howard ordinal, so no relative consistency proof is possible. </p>