2010-01-23 17:41:08 8 Comments

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

### Related Questions

#### Sponsored Content

#### 1 Answered Questions

### [SOLVED] Does every model of ZF-foundation have an extension, with no new well-founded sets, where every set is bijective with a well-founded set?

**2018-05-15 13:29:14****Joel David Hamkins****635**View**15**Score**1**Answer- Tags: set-theory lo.logic axiom-of-choice mathematical-philosophy

#### 8 Answered Questions

### [SOLVED] Why should we believe in the axiom of regularity?

**2015-09-29 18:31:42****Wojowu****5399**View**47**Score**8**Answer- Tags: lo.logic set-theory mathematical-philosophy

#### 1 Answered Questions

### [SOLVED] Is $\in$-induction provable in first order Zermelo set theory?

**2018-11-03 17:54:48****Zuhair Al-Johar****262**View**2**Score**1**Answer- Tags: set-theory lo.logic induction transfinite-induction

#### 2 Answered Questions

### [SOLVED] Consequences of foundation/regularity in ordinary mathematics (over ZF–AF)?

**2018-05-30 16:46:43****Peter LeFanu Lumsdaine****403**View**10**Score**2**Answer- Tags: set-theory lo.logic foundations

#### 2 Answered Questions

### [SOLVED] Does foundation/regularity have any categorical/structural consequences, in ZF?

**2018-05-12 14:28:57****Peter LeFanu Lumsdaine****685**View**14**Score**2**Answer- Tags: set-theory lo.logic foundations categorical-logic

#### 0 Answered Questions

### Can ZF be interpreted in a theory axiomatized by a version of replacement and infinity?

**2018-01-18 17:40:58****Zuhair Al-Johar****238**View**3**Score**0**Answer- Tags: set-theory lo.logic

#### 1 Answered Questions

### [SOLVED] Can epsilon-induction be derived from the transitive closure operator?

**2016-05-06 19:18:37****L. C.****207**View**0**Score**1**Answer- Tags: lo.logic set-theory

#### 0 Answered Questions

### A question regarding forcing in $NGBC^{-f}$+$BAFA$

**2015-10-09 06:49:02****Thomas Benjamin****109**View**3**Score**0**Answer- Tags: lo.logic set-theory forcing

#### 1 Answered Questions

### [SOLVED] Some constructive versions of the Continuum Hypothesis are false. Are any true, or open?

**2010-06-13 16:46:54****Daniel Mehkeri****811**View**11**Score**1**Answer- Tags: lo.logic constructive-mathematics set-theory

#### 3 Answered Questions

### [SOLVED] A rigid type of structure that can be put on every set?

**2009-11-18 04:20:43****Mike Shulman****686**View**11**Score**3**Answer- Tags: ct.category-theory lo.logic

## 3 comments

## @Daniel Mehkeri 2010-06-13 23:13:44

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:

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.

## @Mike Shulman 2010-06-14 04:55:47

Well, that seems pretty definitive. Thanks!

## @François G. Dorais 2010-01-27 03:57:31

Let KP

^{0}be the induction-free fragment of KP. That is, the axioms of KP^{0}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 KP

^{0}.Σ-Reflection.For every Σ-formula KP^{0}⊦ φ ↔ ∃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

^{0}⊦ ∀u∈x∃vφ(u,v) →∃y∀u∈x∃v∈yφ(u,v).Δ-Separation.For every Σ-formula φ(u) and every Π-formula ψ(u),KP

^{0}⊦ ∀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

^{0}+ 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

^{0}+ 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^{0}+ Reg and I is a Σ-cut in A, then A_{I}= {x ∈ A : rk(x) ∈ I} is a model of KP^{0}+ Reg.Sketch of proof.The main point of contention is Δ_{0}-collection. Suppose that φ(u,v) is a Δ_{0}-formula such that A_{I}⊧ ∀u∈x∃vφ(u,v). Consider the set of ordinalsJ = {α ∈ 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

^{0}that satisfies Σ-induction. Unfortunately, there are models of KP^{0}+ 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^{0}that satisfies Π-induction and I is any cut of A, then A_{I}is a model of KP^{0}.(Π-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 ZambellaFoundation 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 KP^{0}(without transitive closures). This is complemented by Antonella Mancini and Domenico ZambellaA 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.## @Mike Shulman 2010-01-30 16:30:33

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?

## @François G. Dorais 2010-01-30 18:07:54

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.

## @Mike Shulman 2010-01-27 02:29:29

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.

## @François G. Dorais 2010-01-27 03:59:08

I was putting final touches on my post when I saw this! Note that Mathias' KP assumes Pi_1-induction.