Generally, a binary relation ≺ on a set

∀*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*=∅

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

∀*A*⊂*X*,
(∀*x*∈*X*,
[*x*] ⊂ *A* ⇒ *x*∈*A*)
⇒ *y*∈*A*

∀*A*⊂*X*, *y*∈*A* ⇒ ∃*x*∈*A*,
*A*∩ [*x*] = ∅

Indeed such a sequence contradicts well-foundedness as Im

Similarly to the concept of term with a root *x*, we have the set *T _{x}*
that is the transitive closure of {

*u*_{0}=*y* ∧ *u _{n}*=

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

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.

∀*x*,*y*∈*X*, (∀*z*∈*X*,
*z*≺*x* ⇔ *z*≺*y*) ⇒ *x*=*y*.

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 ℘(

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

For example, to see that

A simple modification (similarly to the distinction of variables in drafts) gives models

For simplicity, we shall only discuss here universes only made of sets and eventually elements, but not anything else like functions.

A problem arises to formalize the well-foundedness of a universe

∀*A*, *A*≠∅ ⇒ ∃*x*∈*A*,
*A*∩*x* = ∅

The condition for a set

From set theory we can get

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

Any use of this axiom will only apply it to some family of well-founded systems (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 systemX_{i}, ≺_{i})_{i∈I}, indexed by a setI. Then the sum of this family forms itself a well-founded system, which can be condensed into an extensional one, where all (X_{i}, ≺_{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 copyYcan be changed into a set of sets related by ∈, by the modification of the predicate ∈ giving to each elementyofYthe role of the set [y], itself left as a pure element.∎

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.1. Second-order structures and invariants

5.2. Second-order logic

5.3.**Well-foundedness**

5.4. Ordinals and cardinals

5.5. Undecidability of the axiom of choice

5.6. Second-order arithmetic

5.7. The Incompleteness Theorem

More philosophical notes :
5.2. Second-order logic

5.3.

5.4. Ordinals and cardinals

5.5. Undecidability of the axiom of choice

5.6. Second-order arithmetic

5.7. The Incompleteness Theorem