One way to state the axiom of foundation is that the $\in$ relation on any transitive set is well-founded in the following sense:

  • A relation $(X,\prec)$ is well-founded if for any subset $S\subseteq X$ which is inductive, in the sense that $y\in S$ for all $y\prec x$ implies $x\in S$, in fact $S=X$.

This is classically equivalent to the more usual definition, but constructively more reasonable. Now in constructive set theories such as CZF, one often finds a different axiom of "foundation" called set-induction or epsilon-induction:

  • 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$.

This certainly implies that $\in$ is well-founded on any transitive set in the sense above, and the converse is true if 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$.

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 think 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.

(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.)

  • $\begingroup$ Can you still show that transitive closures exist without omega? $\endgroup$ Jan 23, 2010 at 22:43
  • $\begingroup$ The formulation of CZF_0 usually includes strong induction for omega. See the Aczel and Rathjen <a href=ml.kva.se/preprints/meta/… on Constructive Set Theory</a>. $\endgroup$ Jan 23, 2010 at 23:54
  • $\begingroup$ What if we ignore the constructivism angle---what happens with KP? Can one show that KP with the set-version of Foundation is equivalent to KP with the scheme version of Foundation? $\endgroup$ Jan 24, 2010 at 0:09
  • $\begingroup$ For KP, I'm pretty sure the answer is no. Some kind of Harrison pseudowellordering argument should work pretty well. $\endgroup$ Jan 24, 2010 at 4:06
  • 1
    $\begingroup$ Can you give me a reference to learn about "Harrison pseudowellordering argument"? $\endgroup$ Jan 24, 2010 at 4:11

3 Answers 3


Let KP0 be the induction-free fragment of KP. That is, the axioms of KP0 are extensionality, pairing, union, Δ0-separation, Δ0-collection, and (since I see no way of proving this from the other axioms) the existence of transitive closures.

Following Barwise, I define the class of Σ-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 Π-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 Σ-formula φ is canonically equivalent to a Π-formula and vice versa; I will identify ¬φ with its canonical equivalent without further comment.

The following three facts are standard in KP. The usual proofs actually go through in KP0.

Σ-Reflection. For every Σ-formula KP0 ⊦ φ ↔ ∃aφ(a), where φ(a) is obtained from φ by replacing every unbounded quantifier ∃x by the corresponding bounded quantifier ∃x∈a.

Σ-Collection. For every Σ-formula φ(u,v),

KP0 ⊦ ∀u∈x∃vφ(u,v) →∃y∀u∈x∃v∈yφ(u,v).

Δ-Separation. For every Σ-formula φ(u) and every Π-formula ψ(u),

KP0 ⊦ ∀u∈x(φ(u) ↔ ψ(u)) → ∃y∀u∈x(u ∈ y ↔ φ(u)),

where y does not occur free in φ nor ψ.

Instead of Mike Shulman's foundation axiom, I will use the classically equivalent regularity axiom:

(Reg) x ≠ ∅ → ∃y∈x(x∩y = ∅).

This axiom already implies a certain amount of induction because of Δ-separation.

Δ-Induction. For every Σ-formula φ(u) and every Π-formula ψ(u),

KP0 + Reg ⊦ ∀u(φ(u) ↔ ψ(u)) → (∀u(∀v∈uφ(v) → φ(u)) → ∀uφ(u)).

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 KP0 + Reg. A cut in A is a proper initial segment I of the ordinals of A which has no least upper bound; a Σ-cut (resp. Π-cut) is one which can be defined by a Σ-formula (resp. Π-formula).

Σ-Cut Lemma. If A is a model of KP0 + Reg and I is a Σ-cut in A, then AI = {x ∈ A : rk(x) ∈ I} is a model of KP0 + Reg.

Sketch of proof. The main point of contention is Δ0-collection. Suppose that φ(u,v) is a Δ0-formula such that AI ⊧ ∀u∈x∃vφ(u,v). Consider the set of ordinals

J = {α ∈ A : ∃u∈x∀v(rk(v) < α → ¬φ(u,v))}.

This is a Π-definable initial segment of I. We cannot have I = J, since that would violate Δ-induction. Pick β ∈ I \ J. Working in A, we can find a set y such that

∀u∈x∃v∈y(rk(v) < β ∧ φ(u,v)).

If necessary, we can cut down y so that rk(y) ≤ β and hence y ∈ AI. ∎

If A has a minimal Σ-cut, then this gives a model of KP0 that satisfies Σ-induction. Unfortunately, there are models of KP0 + Reg without minimal Σ-cut.

Now, on the positive side a minor twist of the proof of the Σ-cut lemma gives the following.

Π-Cut Lemma. If A is a model of KP0 that satisfies Π-induction and I is any cut of A, then AI is a model of KP0.

(Π-induction implies that the Π set J defined as above must have a least upper bound β ∈ I. The rest of the proof is identical.)

So when A satisfies Π-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 ω.

When I have a chance, I'll try to add examples showing that you can't do better than the Σ-cut lemma and the Π-cut lemma.

Addendum. I just stumbled across two papers that address these questions. The first paper is by Domenico Zambella Foundation versus induction in Kripke-Platek set theory [J. Symb. Logic 63 (1998), MR1665739] where it is shown that foundation implies open-induction, but not Σ1-induction over KP0 (without transitive closures). This is complemented by Antonella Mancini and Domenico Zambella A Note on Recursive Models of Set Theories [Notre Dame J. Formal Logic 42 (2001), MR1993394] where they generalize Tennenbaum's Theorem by showing that fragments of KP which prove Σ1-induction have no computable models other than the standard one.

  • $\begingroup$ Thanks! I'm not too familiar with arguments involving lots of Σs and Πs, so I need some help understanding this. I think I follow the Σ-cut lemma, but why does a minimal Σ-cut give a model of KP⁰ that satisfies Σ-induction? $\endgroup$ Jan 30, 2010 at 16:30
  • $\begingroup$ There is a little syntactic trick involved. Any Sigma-cut in a Sigma-definable initial model is also a Sigma-cut in the larger model by constraining the witnesses to existential quantifiers to stay within the smaller model. Therefore, when I is the minimal Sigma-cut, the initial model A_I has no proper Sigma-cut. $\endgroup$ Jan 30, 2010 at 18:07

Late answer: NO. At least with respect to CZF.

CZF with Set Induction has proof-theoretic ordinal the Bachmann-Howard ordinal.

CZF without Set Induction is weaker. Can't think of a direct reference, but:

  • Crosilla & Rathjen "Inaccessible Set Axioms may have little consistency strength"

It is shown that CZF without set induction but with an inaccessible set axiom has proof-theoretic ordinal $\Gamma_0$.

This is strictly less than the Bachmann-Howard ordinal, so no relative consistency proof is possible.

  • $\begingroup$ Well, that seems pretty definitive. Thanks! $\endgroup$ Jun 14, 2010 at 4:55

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.

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.

  • $\begingroup$ I was putting final touches on my post when I saw this! Note that Mathias' KP assumes Pi_1-induction. $\endgroup$ Jan 27, 2010 at 3:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.