Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Epsilon-induction
Summary
In set theory, -induction, also called epsilon-induction or set-induction, is a principle that can be used to prove that all sets satisfy a given property. Considered as an axiomatic principle, it is called the axiom schema of set induction.
The principle implies transfinite induction and recursion.
It may also be studied in a general context of induction on well-founded relations.
The schema is for any given property of sets and states that, if for every set , the truth of follows from the truth of for all elements of , then this property holds for all sets.
In symbols:
Note that for the "bottom case" where denotes the empty set , the subexpression is vacuously true for all propositions and so that implication is proven by just proving .
In words, if a property is persistent when collecting any sets with that property into a new set (and this also requires establishing the property for the empty set), then the property is simply true for all sets. Said differently, persistence of a property with respect to set formation suffices to reach each set in the domain of discourse.
One may use the language of classes to express schemata.
Denote the universal class by .
Let be and use the informal as abbreviation for .
The principle then says that for any ,
Here the quantifier ranges over all sets.
In words this says that any class that contains all of its subsets is simply just the class of all sets.
Assuming bounded separation, is a proper class. So the property is exhibited only by the proper class , and in particular by no set. Indeed, note that any set is a subset of itself and under some more assumptions, already the self-membership will be ruled out.
For comparison to another property, note that for a class to be -transitive means
There are many transitive sets - in particular the set theoretical ordinals.
If is for some predicate , then with ,
where is defined as .
If is the universal class, then this is again just an instance of the schema.
But indeed if is any -transitive class, then still and a version of set induction for holds inside of .
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.