4.6. Well-foundedness

Well-founded relations

The concept and properties of well-founded relations are a straightforward generalization of the work we did with algebraic drafts, extracting from these structures the precise aspects which ensured the validity of these constructions (dropping the precise use of an algebraic language). Namely from drafts structure, all we need is the binary relation ≺ = txOD Im lx, i.e. xy ⇔ (yODx∈Im ly). We can also ignore variables, reinterpreted as constants, leading to an equivalent characterisation of well-foundedness just like (Ind) is equivalent to (Ind1).
Generally, a binary relation ≺ on a set X is called well-founded when it satisfies the following equivalent conditions, abbreviating by [ ] its curried form ⃖≺ (so that xyx∈[y]):

AX, (∀xX, [x] ⊂ AxA) ⇒ A=X
AX, AX ⇒ ∃xX\A, [x]⊂A
AX, A≠∅ ⇒ ∃xA, A∩[x] = ∅
AX, A ⊂ ≺(A) ⇒ A=∅

Well-founded relations are irreflexive and antisymmetric.
Like we get a minimal algebra from any algebra by taking its minimal sub-algebra, we get a well-founded relation from any binary relation ≺ on a set X by restriction to the set of well-founded elements y, equivalently characterized by

AX, (∀xX, [x] ⊂ AxA) ⇒ yA
AX, yA ⇒ ∃xA, A∩ [x] = ∅

Well-founded relations (resp. elements x) have no descending sequence, that is uX such that ∀n∈ℕ, un+1un (resp. with moreover u0 = x).
Indeed such a sequence contradicts well-foundedness as Im u≠∅ and ∀y∈ Im u, Im u∩[y]≠∅.

Transitive closure

Similarly to the concept of co-stability (sub-draft), a subset K of a relational system (X,≺) is called transitive if ∀x,yX, xyKxK. In particular an element zX is called transitive when the set [z] is transitive, as this looks like a formula of transitivity for ≺. It is equivalent to the co-stability (like sub-drafts) of K, i.e. (yK ⇒ [y]⊂K). As this property is stable by intersection, the transitive closure of a set K, is the smallest transitive set including it.

Similarly to the concept of term with a root x, we have the set Tx that is the transitive closure of {x}, obtained from that of [x] by adding there x itself. It is made of all y such that there exists a finite sequence u with some number n∈ℕ of steps by ≺ from y to x:

u0=yun=x ∧ ∀i<n, uiui+1.

Now, a relational system is well-founded if and only if all its elements are well-founded; and as can be easily shown, an element x is well-founded if and only if the restriction of ≺ to Tx is well-founded.

Well-founded recursion

For any well-founded relation ≺ on a set X, any set E and any Φ : ∐xX E[x]E, there exists a unique h : XE such that ∀xX, h(x) = Φ(x,h|[x]).

The case of interpretation of drafts in algebras comes as Φ(x,u) = σ(x)E(ulx). The general case admits essentially the same proof as we gave for the algebraic case, so we shall not repeat it here, especially as more interesting variants of this proof will be seen later:

Models of set theory

Among possible recursions along the well-founded relation of an algebraic draft, their interpretations in algebras were particular cases in the sense that from (x,u), the function Φ only used σ(x), ulx and the algebraic structure of E. This letting Φ only depend on the structure of the draft, not being attached to a particular draft, makes it invariant by isomorphism between drafts, and quotientable by condensation.

Now let us focus on a more particular case of recursion obtained by further reducing the sensitivity of Φ: applying to the structure of algebras the same simplification LE∋(s,u) ↦ Im u ∈ ℘(E) by which drafts were reduced to well-founded relations, will make interpretations more generally invariant by any change of domain which preserves the well-founded relation.
Let us call set-algebra a system (E,φ) where φ : ℘(E) → E, from which we define Φ(x,u) = φ(Im u). In fact Dom φ may not be all ℘(E), but just needs to contain all possible Im u for functions u from some [x] to E. For example this may be the set of all finite subsets of E if all sets [x] are finite.

For that use, the quality for a well-founded relation ≺ to play the same role as that of condensed drafts, is the injectivity of x↦[x]. Such relations are called extensional, as this condition is similar to the Axiom of Extensionality, replacing ∈ by ≺ :

x,yX, (∀zX, zxzy) ⇒ x=y.

There is also a unique condensation of any well-founded system (X, ≺) preserving its interpretations in set-algebras: its equivalence relation on X is recursively defined in its curried form as the interpretation of X in the set-algebra P = ℘(X) with structure ℘(P)∋A↦{xX | [x]⊂ ⋃A ∧ ∀BA, B∩[x] ≠ ∅}.
Condensed drafts became term algebras when their injective stuff was bijective, letting the algebraic structure be defined by the inverse. Now trying to do the same, to serve both as a final well-founded system and an initial set-algebra, we cannot make φ bijective from ℘(X) to X, due to Cantor's theorem. Still we can look for some weaker conditions leading to similar properties.
A general idea is that such systems will be models of some set theory, where ≺ plays the role of ∈. While term algebras are essentially unique, looking after similar properties won't make set theory complete either semantically nor logically, but can reduce some of the chaotic diversity of shapes of universes which would otherwise occur.
Thanks to the completeness theorem, the unprovability of a formula in a theory, respectively its irrefutability also called "consistency" (the consistency of the theory where it is added as an axiom), amounts to the existence of models where it is false (resp. true). For set theories and other founding theories, whose consistency cannot be proven in the absolute as we shall see by the incompleteness theorem, we can only talk about the relative consistency of a theory, or of a statement in a theory, which means showing that it is consistent if the previous theory was. Relative consistency results are usually proven by using a model of the old theory to build a model of the new one.
For example, to see that finite set theory is consistent relatively to arithmetic, we can make a countable universe whose objects are all its own finite sets, by means of a bijection between ℕ and the set of all its finite subsets. A natural one is given by the binary representation of natural numbers, where for example {1,2}=6. This forms a well-founded relation.
A simple modification (similarly to the distinction of variables in drafts) gives models U of set theories also admitting pure elements as objects : by a bijection between some class of subsets of U (as viewed from the outside), and a subset of U serving as the class of its "sets". For example a well-founded countable model of the finite set theory with n pure elements represented by numbers lower than n, is given by defining xn+y as "x belongs to the binary representation of y". It is also easy to define a countable model with an infinity of pure elements.
For simplicity, we shall only discuss here universes only made of sets and eventually elements, but not anything else like functions.

Axiom of foundation

The above suggests to require of models of set theory, to have ∈ well-founded, thus allowing to defining something on every set recursively, as determined by what is attributed to its elements. This would formalize the intuitive idea that such universes come as "built" in order, starting from the empty set and progressively adding there sets of already existing objects. From any universe we can make a well-founded one as the meta-set of all sets which are well-founded (in the above sense of well-founded element of a set with a relation, here an element of the universe with the predicate ∈), though care may be needed on details depending on the truths (axioms) we want to preserve.
A problem arises to formalize the well-foundedness of a universe U, which is basically a second-order requirement (using ∀ over ℘(U)), into axioms of set theory which need to be first-order formulas. Before turning such a second-order axiom into a schema of axioms we may already try it over two kinds of meta-subsets of the universe: the sets, and the complements of sets. Here, one side turns out to not be informative, as, when A is a set, the formula (∀B, BABA) is always false by Cantor's theorem. But the other side is actually called the axiom of foundation (AF):

A, A≠∅ ⇒ ∃xA, Ax = ∅

Its relative consistency easily comes by taking the meta-set of all sets E which seem "well-founded" for the similar expression (∀A, EA ⇒ ∃xA, Ax = ∅), but the question remains whether it actually suffices to make the universe well-founded. To answer this, we need the concept of transitive closure.
The condition for a set x to be well-founded would be expressed by AF where A ranges over all meta-subsets of its transitive closure Tx which is a priori only defined as a meta-set. Finally for A to actually range there in AF, we just need Tx to be a set, whose powerset we shall then trust to do the job. So, are all Tx sets ?
From set theory we can get Tx as the union of the sequence u recursively defined by u0=x ∧ ∀n∈ℕ, un+1 = ⋃un... if only such a sequence exists. Otherwise, we may add as an axiom that Tx is a set ... if justified from the intended well-foundedness of the universe: from the recursive expression Tx = {x}∪⋃yx Ty, we could deduce that Tx is a set when all Ty are sets... if only {Ty | yx} was accepted as a set in the universe. But this does not result either from our previously accepted axioms, since this expression is a priori only defined on the meta level.
But a good reason to add it as an axiom, is to make the universe actually useful in its intended role as a union of representatives of all extensional well-founded relations, where recursion would be well-defined... by formulas which make sense inside the same universe without the help of any special language for it. Namely, to define the image of any x by any recursion, requires to check its validity by using, as a function, the interpretation of that recursion with domain at least Tx, which must thus be a set. May that mean to add Tx to the universe, or to remove x from there when Tx cannot be found.

More needed axioms

Any well-founded system (X, ≺) must have its image (unique interpretation) among sets related by ∈. This axiom is relatively consistent for the following reason.
Any use of this axiom will only apply it to some family of well-founded systems (Xi, ≺i)iI, indexed by a set I. Then the sum of this family forms itself a well-founded system, which can be condensed into an extensional one, where all (Xi, ≺i) are interpreted. Let us admit here that without contradiction, we can assume the existence of a copy (Y, ≺) of that extensional system made of pure elements. Now that copy Y can be changed into a set of sets related by ∈, by the modification of the predicate ∈ giving to each element y of Y the role of the set [y], itself left as a pure element.∎
A similar trick shows the relative consistency of the negation of the foundation axiom : from any extensional but non-well-founded relation we can create a copy related by ∈ as well.

Now well-founded recursion can process from any system Tx of sets related by ∈ in particular, just like from any well-founded system in general, with target any given set-algebra known to be a set. However, to also work with target the whole universe, is a quite stronger requirement : it implies the just mentioned ability of sets to represent all well-founded relations (by recursion from a well-founded set into the universe) but is not relatively consistent anymore, in particular for the already mentioned sequence of powersets of ℕ. But this, as well as the existence of the transitive closure of any set, are just a particular cases of the even much stronger schema of replacement that is the last part of ZF, which will be discussed later.
Set theory and foundations of mathematics
1. First foundations of mathematics
2. Set theory (continued)
3. Algebra 1
4. Model Theory
4.1. Finiteness and countability
4.2. The Completeness Theorem
4.3. Non-standard models of Arithmetic
4.4. How theories develop
4.5. Second-order logic
4.6. Well-foundedness
4.7. Ordinals and cardinals
4.8. Undecidability of the axiom of choice
4.9. Second-order arithmetic
4.10. The Incompleteness Theorem