Is set-induction relatively consistent?

Question

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

Answer 1

Let KP⁰ be the induction-free fragment of KP. That is, the axioms of KP⁰ are extensionality, pairing, union, Δ₀-separation, Δ₀-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 KP⁰.

Σ-Reflection. For every Σ-formula KP⁰ ⊦ φ ↔ ∃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),

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

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

KP⁰ ⊦ ∀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),

KP⁰ + 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 KP⁰ + 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 KP⁰ + Reg and I is a Σ-cut in A, then A_I = {x ∈ A : rk(x) ∈ I} is a model of KP⁰ + Reg.

Sketch of proof. The main point of contention is Δ₀-collection. Suppose that φ(u,v) is a Δ₀-formula such that A_I ⊧ ∀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 ∈ A_I. ∎

If A has a minimal Σ-cut, then this gives a model of KP⁰ that satisfies Σ-induction. Unfortunately, there are models of KP⁰ + 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 KP⁰ that satisfies Π-induction and I is any cut of A, then A_I is a model of KP⁰.

(Π-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 Σ₁-induction over KP⁰ (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 Σ₁-induction have no computable models other than the standard one.

Answer 2

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.

Answer 3

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.