5.3. 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 ≺ = t∐x∈OD
Im lx, i.e. x≺y ⇔
(y∈OD ∧ x∈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 x≺y ⇔ x∈[y]):
∀A⊂X, (∀x∈X,
[x] ⊂ A ⇒ x∈A) ⇒ A=X
∀A⊂X, A≠X
⇒ ∃x∈X\A, [x]⊂A
∀A⊂X, A≠∅ ⇒ ∃x∈A,
A∩[x] = ∅
∀A⊂X, 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
∀A⊂X,
(∀x∈X,
[x] ⊂ A ⇒ x∈A)
⇒ y∈A
∀A⊂X, y∈A ⇒ ∃x∈A,
A∩ [x] = ∅
Well-founded relations (resp. elements x)
have no descending sequence, that is u∈Xℕ such that ∀n∈ℕ,
un+1≺un (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,y∈X, x≺y∈K ⇒ x∈K.
In particular an element z∈X 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. (y∈K ⇒ [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=y ∧ un=x ∧
∀i<n, ui≺ui+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 Φ : ∐x∈X
E[x] → E, there exists a unique
h : X→E such that ∀x∈X,
h(x) = Φ(x,h|[x]).
The case of interpretation of drafts in algebras comes as
Φ(x,u) = σ(x)E(u০lx).
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:
- an expression of recursive
sequences (X=ℕ) with minimal assumptions on the framework;
- another elegant proof comes when X is a term algebra (using minimal subalgebras in products);
- a general one will follow the study
of Galois connections, with more details on the properties of well-foundedness.
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),
u০lx 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
L⋆E∋(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,y∈X, (∀z∈X,
z≺x ⇔ z≺y) ⇒ 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↦{x∈X | [x]⊂ ⋃A ∧ ∀B∈A,
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 defining ∈ as
the Bit predicate
expressing the binary
representation of natural numbers, where for example {1,2}=6. This
forms a well-founded relation. (Technical details
were investigated by Richard Kaye and Tin Lok Wong)
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 x≺n+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,
B⊂A ⇒ B∈A) is always false by Cantor's theorem.
But the other side is actually called the axiom of foundation (AF):
∀A, A≠∅ ⇒ ∃x∈A,
A∩x = ∅
Its relative consistency easily comes by taking the meta-set of all
sets E which seem "well-founded" for the similar expression
(∀A, E∈A ⇒ ∃x∈A, A∩x = ∅),
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}∪⋃y∈x Ty, we
could deduce that Tx is a set when all
Ty are sets... if only {Ty |
y∈x} 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)i∈I,
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. Arithmetic and first-order foundations
5. Second-order foundations
More philosophical notes :