Set theory

ZF without foundation consists of the axioms of Zermelo–Fraenkel set theory with the Axiom of foundation omitted. Ordinal-indexed transfinite recursion still defines the cumulative hierarchy. Its union is the well-founded part and need not include all ambient sets.

Foundation in the cumulative hierarchy without ambient Foundation

The cumulative hierarchy is a transitive class even without the ambient Axiom of foundation. If

a

is a nonempty member, choose the least ordinal

α

with

a \cap V_{α} \neq = \emptyset

. It is a successor

β + 1

. An element

x

of that intersection is a subset of

V_{β}

, while

a

has no element in

V_{β}

, so

a \cap x = \emptyset

. This proves internal Foundation. If the hierarchy also satisfies the other ZF axioms, restricting every quantifier of a finite ZF proof to this definable class translates it into a proof from ZF without foundation. Thus adjoining Foundation preserves consistency relative to the remaining axioms.

Set-theoretic limit

For a sequence of sets, the limit superior of sets consists of points belonging to infinitely many members, while the lower limit consists of points belonging to every sufficiently late member. If the two sets coincide, their common value is the set-theoretic limit.

Limit superior of sets ( $lim sup_{n} E_{n} = ⋂_{N} ⋃_{n \geq N} E_{n}$ )

Membership means that for every index

N

there is a later

n \geq N

with

x \in E_{n}

, equivalently membership for infinitely many indices. If

\sum_{n} μ (E_{n}) < \infty

, countable subadditivity gives

μ (lim sup E_{n}) \leq \sum_{n \geq N} μ (E_{n}) \to 0

. This is the measure form of the first Borel-Cantelli lemma, and requires no independence assumption.

Russell's paradox ( $R \in R ⟺ R \in / R$ )

Unrestricted formation of a set

R = {x : x \in / x}

contradicts its own membership condition: substituting

R

for

x

gives the displayed equivalence. Thus a predicate cannot always define a set of all objects satisfying it. Restricted set comprehension forms a subset of a previously given set, avoiding this argument. The contradiction does not assert that a set whose elements happen not to contain themselves is impossible; it rules out the universal collection with exactly the specified membership condition.

Barber paradox

For a binary relation

S

, no object

b

can satisfy

S (b, p) \leftrightarrow \neg S (p, p)

for every

p

. Putting

p = b

would give

s \leftrightarrow \neg s

for

s = S (b, b)

. The forward direction derives

\neg s

by a negation introduction subproof assuming

s

; the reverse direction then gives

s

, a contradiction. Thus this argument even avoids needing the law of excluded middle. The familiar interpretation reads

S (b, p)

as “

b

shaves

p

”; the logical obstruction is self-application rather than a physical peculiarity of shaving.

Urelement

An urelement is an object permitted alongside sets, with no members, distinguished from the empty set by an atom or set predicate. Extensionality is restricted to sets, so distinct atoms need not be equal merely because they have no members. An atom is different from a Quine atom, which is a set with a self-member. In simple typed set theory with atoms, each sort may contain urelements in addition to the objects representing subsets of the preceding sort.

Basic Fraenkel permutation model

Start with a well-founded universe of sets over an infinite set

A

of urelements. The full symmetric group of

A

acts recursively on sets. Retain the objects all of whose descendants have a finite support in a permutation action. This class satisfies set-extensionality, foundation, infinity, pairing, union, separation, replacement and its internal power set axiom. A definable functional image has the finite union of the supports of its domain and parameters as a support; uniqueness makes the image invariant. The family of two-element subsets of

A

has no choice function: a transposition of two atoms outside the function's finite support fixes their pair and moves either possible choice. For untyped membership with extensionality merely restricted to nonempty objects, atoms are also vacuous subsets; add all atoms to each internal power-set object.

Hereditarily locally small membership model ( $B_{λ}$ )

For a strong-limit cardinal

λ

of countable cofinality, define

B_{λ} = {x : \forall y \in TC ({x}) (∣ y ∣ < λ)} .

Here smallness bounds every individual membership extension; it does not bound the cardinality of the entire transitive closure. The transitive class

B_{λ}

satisfies all ZF axioms except possibly the Axiom of union: functional images have fewer than

λ

elements, and the power set of a set of size

μ < λ

has size

2^{μ} < λ

. These facts give Axiom schema of replacement and Axiom of power set; pairs and definable subsets also remain locally small. For

λ = ℶ_{ω}

, the countable set

{V_{ω + n} : n < ω}

belongs to

B_{λ}

, but its union

V_{ω + ω}

has size

λ

and does not. This gives an explicit relative-independence model for the Axiom of union.

New Foundations

New Foundations uses ordinary extensionality and comprehension restricted to stratified formulas. Its atom-permitting weakening is New Foundations with urelements.

New Foundations with urelements ( $NFU$ )

NFU has a universal domain, a predicate

S

distinguishing sets from atoms, extensionality restricted to sets, and comprehension for stratified formulas. Atoms have no members. Every stratified predicate has a set extension, including the always-false predicate, so there is a distinguished empty set even when atoms exist. Permitting atoms removes the full-extensionality obstacle in New Foundations.

Type-shifting automorphism ( $j : D_{i} ⟶ D_{i + 1}$ )

For an integer-indexed typed model, a type-shifting automorphism is a bijection from each type to the next preserving equality, adjacent-type membership and the set predicates. On type zero define

x E y

x \in j (y)

. Stratified formulas are translated by sending a variable of type

i

j^{i} (x)

. Typed comprehension then gives the untyped comprehension of NFU. Such an automorphism is external; formulas containing it are not included in the typed comprehension scheme.

Rank-shifting automorphism construction of NFU

In a model of ZFC, choose an external automorphism

j

and an ordinal

α

with

j (α) > α

. Set

D_{i} = V_{j^{i} (α)}

for integer

i

, and declare the sets of type

i + 1

to be its objects that are subsets of

D_{i}

. Ordinary membership between successive types satisfies typed comprehension and set-extensionality. The automorphism shifts all types, yielding NFU by the type-zero collapse. A Skolem hull of integer-indexed increasing ordinal indiscernibles supplies such a

j

by shifting the indices. The model is externally ill-founded; a transitive well-founded universe cannot have such an automorphism.

Rank-shifting NFU model with explicit set predicate ( $S (y) ⟺ j (y) \subseteq D, x E y ⟺ S (y) \land x \in j (y)$ )

Let

M

be a membership structure satisfying extensionality and every pure-membership separation instance, with an external automorphism

j

and domains

D_{i} = j^{i} (D_{0})

represented by objects of

M

. Suppose every

M

-subset of

D_{i}

is an element of

D_{i + 1}

. Interpret NFU on the objects of

D_{0}

using the displayed set predicate and membership, with all subset statements evaluated in

M

. Atoms have no members, and extensionality applied to

j (y), j (z) \subseteq D_{0}

gives extensionality for sets. A stratified formula becomes an ordinary pure-membership formula by sending each variable of type

i

j^{i} (x)

and restricting its quantifier to

D_{i}

. A set predicate on sort

i

means containment in

D_{i - 1}

; adjacent-sort membership is guarded by containment in the lower domain. Separation yields the extension

X \subseteq D_{i}

, the closure hypothesis places it in

D_{i + 1}

, and

j^{- (i + 1)} (X) \in D_{0}

is the required untyped set. This proves every comprehension instance. The guard is essential: an object not contained in a lower domain can still have some ordinary members there, which must not become members of a typed atom. Internal ranks

V_{j^{i} (α)}

with

j (α) > α

give one instance of these hypotheses; shifted rank objects in an elementary model of an expanded

V_{ω + ω}

give a consistency proof without assuming Con(ZFC).

Rank-indiscernible construction of an NFU model

NFU has a unary predicate

S

for sets, atoms have no members, extensionality applies to sets, and comprehension applies to every stratified formula. A stratification assigns integer types to variables so that equality uses equal types and

x \in y

requires

type (y) = type (x) + 1

. A unary set predicate adds no type difference.

Start with the actual set structure

B = (V_{ω + ω}, \in)

. This structure satisfies extensionality and every pure-membership separation instance: the subset defined in a set

a

of rank below

ω + ω

still has rank below

ω + ω

. We do not assert that

B

satisfies replacement or all of ZFC. Expand it by Skolem functions. In it use the sequence of rank objects

V_{ω + n + 6}

n < ω

. For two such objects

d < e

in sequence order, we have

d ⊊ e, \forall x (x \subseteq d ⟹ x \in e),

with quantifiers in

B

. The second statement holds because every subset of

V_{α}

belongs to

V_{α + 1}

, and the later rank is at least

α + 1

Introduce constants

d_{i}

i \in Z

, and require them to be order indiscernibles in the Skolem language, satisfying these two assertions whenever

i < j

. Also require

V_{ω + 5} \subseteq d_{i}

for every

i

; this fixed rank object is first-order definable in

B

. Every finite part of these requirements together with

Th (B^{*})

is satisfiable: color finite increasing tuples of the original rank sequence by the truth values of the finitely many formulas mentioned, and use Ramsey's theorem to get a homogeneous subsequence. The rank assertions hold for every increasing tuple there. The compactness theorem gives a model of the full theory. In its Skolem hull

N

generated by the

d_{i}

, the integer shift extends to an automorphism

j

with

j (d_{i}) = d_{i + 1}

, by the term-transport proof of the Ehrenfeucht-Mostowski theorem. Thus

N

still satisfies extensionality and all pure-membership separation instances, and

N ⊨ \forall x (x \subseteq d_{i} ⟹ x \in d_{i + 1}) (i \in Z) .

(2)

This is a set-sized first-order model; no satisfaction predicate for a proper-class universe is being assumed.

Externally let

D_{i} = {x \in N : N ⊨ x \in d_{i}}

. The automorphism bijects

D_{i}

onto

D_{i + 1}

. Interpret a typed structure with sort

i

equal to

D_{i}

. At sort

i + 1

, declare

y

a set exactly when

N ⊨ y \subseteq d_{i}

; otherwise it is an atom. Define adjacent-sort membership by

x \in_{i} y ⟺ N ⊨ (y \subseteq d_{i} \land x \in y) .

(3)

The guard is necessary: a typed atom might have some ordinary

N

-members in

D_{i}

, and those must not become its typed members. Set-extensionality follows from extensionality in

N

, because the ordinary members of a typed set all lie in

D_{i}

. For any typed formula on sort

i

, its quantifiers can be restricted to the corresponding

d_{l}

, its set predicates replaced by subset assertions, and its memberships replaced by the guarded relation. This is an ordinary pure-membership formula of

N

with finitely many parameters. Separation gives its extension

X \subseteq d_{i}

, and the displayed closure assertion gives

X \in d_{i + 1}

. It is therefore a typed set witnessing comprehension. The automorphism shifts these sorted domains and preserves the set flags and guarded memberships.

Collapse the types onto

D_{0}

. Define

S (y) ⟺ N ⊨ j (y) \subseteq d_{0}, x E y ⟺ S (y) \land N ⊨ x \in j (y) .

(4)

Objects not satisfying

S

have no

E

-members. If two sets have the same

E

-members, their images under

j

are subsets of

d_{0}

with the same ordinary members, so are equal by extensionality of

N

; injectivity of

j

gives equality of the original objects.

To verify every stratified comprehension instance, assign a variable

v

its stratification type

t (v)

and translate its value

a \in D_{0}

j^{t (v)} (a) \in D_{t (v)}

. Equality is preserved. An atomic

E (x, y)

translates to the guarded adjacent-sort membership because

t (y) = t (x) + 1

; the unary predicate

S (y)

translates to

j^{t (y)} (y) \subseteq d_{t (y) - 1}

. Induction on formulas, using the domain bijections for quantifiers, preserves truth. If the free variable

x

has type

t

, typed comprehension produces its extension

X \subseteq d_{t}

, with

X \in d_{t + 1}

. Put

b = j^{- (t + 1)} (X) \in D_{0}

. Then

S (b)

holds, and for every

a \in D_{0}

a E b ⟺ N ⊨ j^{t} (a) \in X ⟺ φ (a, p) .

(5)

This is exactly the required NFU set. No formula containing the external automorphism

j

has been used in a separation or comprehension scheme;

j

only transports values after the pure formula is formed.

The construction also permits the usual infinity requirement. The ordinary

ω

and its successor graph

f

are definable in

N

, hence fixed by

j

, and lie below

V_{ω + 5}

, so belong to all the required domains. Under

E

, the members of

ω

are still its ordinary

N

-members. The new Kuratowski pair satisfies

⟨ x, y ⟩_{E} = j^{- 2} (⟨ x, y ⟩_{N}) .

(6)

Since

j (f) = f

, membership of this pair in

f

under

E

is equivalent to

⟨ x, y ⟩_{N} \in f

. Thus

f

is an internal injection of

ω

into itself omitting zero, giving a Dedekind-infinite set.

We have built a model of NFU, with infinity if it is included in the formulation, in ordinary ZFC metatheory:

ZFC proves the existence of a model of NFU.

(7)

In particular

Con (ZFC) \Rightarrow Con (NFU)

. This proof does not assume

Con (ZFC)

as an additional internal axiom: its starting structure is the set

V_{ω + ω}

, not a model of ZFC.

Stratified formula

A formula is stratified if its variables can be assigned integer types so that equality relates variables of the same type and membership

x \in y

requires

type (y) = type (x) + 1

. Unary set predicates impose no additional difference. Stratification is a syntactic condition; it does not assert that the untyped universe actually has disjoint types. Translating a stratified formula into a typed model permits type-shifting automorphism to recover untyped comprehension.

Simple typed set theory with atoms ( $TSTU$ )

Objects have sorts

0, 1, \dots

, with membership allowed only from sort

i

to sort

i + 1

. A set predicate distinguishes sets from atoms; atoms have no members, extensionality applies to sets, and every well-typed formula defines a set in the next sort by comprehension. First-order models may have only a specified collection of subsets, as in Henkin semantics. For a full finite-type model, take

D_{i} = V_{r_{i}}

at widely separated increasing ranks, represent sets at level

i + 1

P (D_{i}) \subseteq D_{i + 1}

, and treat the remaining objects as atoms under typed membership.

Typical ambiguity ( $ϕ \leftrightarrow ϕ^{+}$ )

Typical ambiguity is the schema asserting that every closed well-typed sentence is equivalent to its uniform type-raise. It is not an assertion that adjacent types have the same cardinality. To obtain finite satisfiability, color finite increasing rank selections by the truth values of the finitely many sentences concerned. The Ramsey's theorem gives a homogeneous rank set; two overlapping windows then have equal truth vectors, yielding the desired type-raise equivalences. The compactness theorem gives a first-order model of the entire schema.

Axiom of pairing ( ${x, y}$ )

For any two sets there is a set containing exactly those two members. Together with other ZFC axioms it permits ordinary ordered-pair coding. Countable-subset closure implies this axiom for the structure of hereditarily countable sets.

Axiom of extensionality ( $(\forall z) (z \in x \leftrightarrow z \in y) ⟹ x = y$ )

Two sets with exactly the same members are equal. In a transitive model, all actual members of its sets are available internally, so ambient extensionality gives the internal axiom as well.

Non-extensional membership model with one atom

Build well-founded coded sets over a single urelement

a

with no members, retaining a distinct empty set. Use the unmodified membership language, so both

a

and the empty set have the same empty extension and extensionality fails. Pairs, unions, separation and functional ranges have set codes, and pure natural numbers give infinity. For the unrestricted Axiom of power set, the power-set code must contain

a

as well as all ordinary subset codes, since the atom is vacuously a subset of every object. Rank gives foundation. Thus the other ZF axioms hold.

Independent family of sets ( $⋂_{j = 1}^{m} A_{j}^{ε_{j}} \neq = \emptyset$ )

A family of subsets of

X

is independent when every finite choice of distinct members and their complements has nonempty intersection. Write

A^{1} = A

and

A^{0} = X ∖ A

in the displayed condition. Every assignment of zero or one to the family then gives a collection with the finite intersection property, which can be extended to an ultrafilter.

Fichtenholz-Kantorovich independent family ( $∣ I ∣ = 2^{∣ X ∣}$ )

For every infinite set

X

there is an independent family of sets consisting of

2^{∣ X ∣}

subsets of

X

. One construction uses a set

D

of pairs

(s, H)

, where

s \subseteq X

is finite and

H \subseteq P (s)

. For each

A \subseteq X

, let

I_{A} = {(s, H) : A \cap s \in H}

. Given distinct

A_{1}, \dots, A_{m}

, choose a finite

s

distinguishing all their traces and choose

H

to contain precisely the traces prescribed to have value one. This realizes every finite Boolean choice. With the axiom of choice,

∣ D ∣ = ∣ X ∣

, so a bijection transports this family to

X

. Its independent assignments give

2^{2^{∣ X ∣}}

distinct ultrafilters.

Almost disjoint family on a regular cardinal ( $A \neq = B ⟹ ∣ A \cap B ∣ < κ$ )

A family of size-

κ

subsets of a set is almost disjoint at

κ

when distinct members have intersection of size less than

κ

. Graphs of a long chain under eventual domination give such a family of size

κ^{+}

κ \times κ

. Transport by a bijection gives a family on

κ

itself.

Essential disjointness of small subfamilies ( $A_{η}^{*} = A_{η} ∖ ⋃_{ν < η} A_{ν}$ )

Any at-most-

κ

subfamily of an almost disjoint family on a regular cardinal becomes pairwise disjoint after deleting fewer than

κ

points from each member. Enumerate it in length at most

κ

and apply the displayed trimming. Each removed part is a union of fewer than

κ

small intersections, so regular cardinal arithmetic bounds it below

κ

Kappa-filtration ( $(A_{α})_{α < κ}$ )

For a set

A

of size an uncountable regular cardinal

κ

, an increasing sequence

(A_{α})_{α < κ}

with union

A

, each

∣ A_{α} ∣ < κ

, and

A_{δ} = ⋃_{α < δ} A_{α}

at every nonzero limit stage.

Club agreement of countable filtrations ( $f [F_{δ}] = G_{δ} on a club$ )

For two kappa-filtrations at

κ = ω_{1}

exhausting sets of size

ℵ_{1}

, any bijection between the sets carries corresponding stages onto one another on a club set of indices. Bound both forward and inverse images at each countable stage by a function

g : ω_{1} \to ω_{1}

. The limit ordinals closed under all earlier

g

-values form a club; continuity gives equality at those ordinals.

Almost disjoint family on omega ( $A \subseteq [ω]^{ω}$ )

A family of infinite subsets of

ω

such that any two distinct members have finite intersection.

Maximal almost disjoint family on omega ( $MAD$ )

An almost disjoint family on omega that cannot be enlarged by another infinite subset while retaining almost disjointness. For the cardinal invariant

a

, one requires the family itself to be infinite; finite partitions otherwise give trivial maximal families.

Almost disjointness number ( $a$ )

The least size of an infinite maximal almost disjoint family on omega. Zorn lemma extends an infinite disjoint family to a maximal one; thus

a \leq 2^{ℵ_{0}}

. The bounding-to-almost-disjointness inequality supplies

b \leq a

Bounding-to-almost-disjointness inequality ( $b \leq a$ )

For an infinite almost disjoint family on omega of size less than the bounding number, select countably many members and remove their intersections with earlier selected members to obtain infinite disjoint sets

C_{n}

. Bound, eventually and simultaneously, the finite intersections of each member with

C_{n}

. Choose one point of each

C_{n}

above its bound. The resulting infinite set is almost disjoint from every original member, proving the family is not maximal. A selected member has one exceptional infinite intersection, which is ignored in its bounding function.

Standard membership model of set theory ( $(M, \in)$ )

A model whose relation symbol for membership is interpreted by actual membership restricted to its domain. If the domain is also transitive, it is a transitive model. Some conventions include this transitivity requirement in the word standard.

Partition relation ( $λ \to (μ)_{β}^{α}$ )

The notation

λ \to (μ)_{β}^{α}

says that every

β

-coloring of the

α

-element subsets of

λ

has a homogeneous subset of order type

μ

. At infinite arity one specifies whether the domain subsets have a fixed cardinality or a fixed order type; the usual finite-arity notation has no such ambiguity.

Finite-symmetric-difference colouring of infinite subsets

Choose a representative

R

of each class of countably infinite sets modulo finite symmetric difference, and colour

A

by the parity of

∣ A △ R ∣

. Removing one element stays in the same class and flips the parity. Every infinite candidate homogeneous set therefore has two countably infinite subsets of opposite colours. With choice, this refutes unrestricted countably infinite-arity positive partition relations on every infinite cardinal.

Erdős-Rado theorem for finite arities ( $ℶ_{r} (λ)^{+} ⟶ (λ^{+})_{λ}^{r + 1}$ )

For an infinite cardinal

λ

and finite

r \geq 0

, put

ℶ_{0} (λ) = λ

and

ℶ_{r + 1} (λ) = 2^{ℶ_{r} (λ)}

. Every

λ

-coloring of

(r + 1)

-element subsets of

ℶ_{r} (λ)^{+}

has a homogeneous subset of size

λ^{+}

. The case

r = 1

is the Erdős-Rado theorem for pairs. For the induction, the end-homogeneous routing tree yields a sequence of length

ℶ_{r - 1} (λ)^{+}

on which the color of an

(r + 1)

-tuple depends only on its first

r

entries. The previous-arity theorem homogenizes those

r

entries. The case

r = 0

is the infinite pigeonhole principle at a successor cardinal.

Closed elementary-submodel construction of an end-homogeneous sequence

Put

θ = (2^{μ})^{+}

for an infinite cardinal

μ

. Choose

M ≺ H_{χ}

of size

2^{μ}

, containing all ordinals below

μ^{+}

, and closed under externally given sequences of length at most

μ

. Such a model is built by

μ^{+}

successive Skolem hull closures, since

(2^{μ})^{μ} = 2^{μ}

. For a coloring of

[θ]^{r + 1}

with at most

μ

colors in

M

, put

β = sup (M \cap θ) < θ

. Recursively choose

x_{α} \in M \cap θ

for

α < μ^{+}

, above all earlier points, so that every earlier

r

-tuple has the same color with

x_{α}

as with

β

. There are at most

μ

constraints, their code belongs to

M

by closure, and

β

witnesses their consistency. The elementary embedding supplies the required witness in

M

. The resulting sequence is end-homogeneous, providing the induction step in the Erdős-Rado theorem for finite arities.

End-homogeneous routing tree ( $∣ T_{α} ∣ \leq λ^{∣ [α]^{r} ∣}$ )

For a coloring of

(r + 1)

-subsets of an ordinal, route a vertex through the least earlier vertices matching its colors on every

r

-subset of previously chosen ancestors. The path stops when the vertex itself is selected. Common path prefixes agree, yielding a set-theoretic tree; a node at level

α

is determined by its color table on

[α]^{r}

. Along a branch, the color of an

(r + 1)

-tuple is independent of its last entry. If the domain has size

(2^{μ})^{+}

and

λ \leq μ

, levels below

μ^{+}

have size at most

2^{μ}

; counting all those levels forces a branch of length

μ^{+}

. If the domain is a regular strong-limit cardinal

κ

, those levels instead have size below

κ

, and the tree property supplies a cofinal branch when needed.

Erdős-Rado theorem for pairs ( $(2^{λ})^{+} ⟶ (λ^{+})_{λ}^{2}$ )

For every infinite cardinal

λ

, every coloring of pairs from

(2^{λ})^{+}

λ

colors has a monochromatic subset of size

λ^{+}

. Construct an end-homogeneous tree by routing a new vertex through the least preceding vertices that match its colors to all previously chosen ancestors. An ancestor's color to every later vertex on a branch is constant. A node at height

α

is determined by its color sequence of length

α

, so levels below

λ^{+}

have size at most

λ^{∣ α ∣} \leq 2^{λ}

. The whole tree has more than

2^{λ}

vertices, forcing a branch of length

λ^{+}

. One of the

λ

ancestor-colors occurs

λ^{+}

times, giving the required set.

Ordinal partition-bound function ( $f (α) = min {β \geq α : \forall ν < α (β \to (α)_{ν}^{2})}$ )

The colors

ν

here range over nonzero cardinals. The Erdős-Rado theorem for pairs makes this function total, and target and color monotonicity make it nondecreasing, with

f (α) \geq α

. If an uncountable cardinal

κ

is closed below itself under

f

, then it is strong limit. Indeed, coloring distinct binary strings of length

λ < κ

by their first differing coordinate uses

λ

colors and has no monochromatic triangle, so

f (λ + 1) > 2^{λ}

. If

κ

also has the tree property, the end-homogeneous tree for any

ν < κ

has levels of size below

κ

and a cofinal branch; regularity makes one color occur

κ

times. Thus

f (κ) = κ

. This distinguishes function closure plus the tree property from the tree property alone.

Finite-subset partition property ( $λ \to (λ)_{β}^{< ω}$ )

The relation

λ \to (λ)_{β}^{< ω}

requires a subset of size

λ

homogeneous at each finite arity. The constant color may depend on the arity.

Small forcing preservation of finite-subset partition properties

If inaccessible

λ

has the finite-subset partition property for every color number below

λ

, forcing of size below

λ

preserves its two-color version. Color ground-model finite sets by their full forcing decision patterns; strong-limit cardinal arithmetic bounds the number of patterns.

Infinite-arity partition relation ( $κ ↛ (ω)_{2}^{ω}$ )

A partition relation whose colored subsets are infinite. For countably infinite arity, choosing representatives modulo finite symmetric difference and coloring its parity shows

κ ↛ (ω)_{2}^{ω}

for every infinite cardinal

κ

Eventual domination ( $f \leq^{*} g$ )

For functions

f, g : ω \to ω

, write

f \leq^{*} g

when

f (n) \leq g (n)

for all sufficiently large

n

. A dominating family is cofinal for this relation.

Eventual domination on a regular cardinal ( $f <^{*} g$ )

For

f, g : κ \to κ

, write

f <^{*} g

when there is

γ < κ

such that

f (δ) < g (δ)

whenever

γ < δ < κ

. For an infinite regular cardinal, suprema of fewer than

κ

ordinals below

κ

remain below it, permitting the long chain under eventual domination construction.

Long chain under eventual domination ( $⟨ f_{ζ} : ζ < κ^{+} ⟩$ )

For every infinite regular cardinal

κ

, there is a strictly eventually increasing sequence of

κ^{+}

functions

κ \to κ

. At stage

0 < ζ < κ^{+}

enumerate predecessors by

e : κ \to ζ

and put

f_{ζ} (δ) = sup_{η < δ} (f_{e (η)} (δ) + 1)

. Regularity bounds each value below

κ

, while any predecessor's index is eventually included in the supremum.

Bounding number ( $b$ )

The least size of a family in

ω^{ω}

having no common bound for eventual domination. Every countable family

(f_{i})

has the bound

g (n) = 1 + max_{i \leq n} f_{i} (n)

, so

ℵ_{1} \leq b \leq 2^{ℵ_{0}}

Dominating family ( $\forall f \exists g \in C f \leq^{*} g$ )

A family

C \subseteq ω^{ω}

such that every

f \in ω^{ω}

is eventually dominated by some

g \in C

Sierpiński decomposition of the plane

A partition

R^{2} = A ⊔ B

in which every vertical section of

A

and every horizontal section of

B

is countable. Swapping the coordinate directions gives the equivalent convention.

Definable continuous hierarchy ( $H_{λ} = ⋃_{α < λ} H_{α}$ )

A definable continuous hierarchy is a definable class function from the ordinals to sets, with increasing levels

H_{α}

and the displayed continuity condition at nonzero limit ordinals. Its union is a definable class in set theory. One often additionally requires transitive sets as levels. Finite collections of first-order formulas reflect along this hierarchy by the reflection theorem for definable hierarchies.

Zermelo–Fraenkel set theory

 2  0

Zermelo–Fraenkel set theory is the usual first-order axiomatization of sets by extensionality, empty set, pairing, union, power set, infinity, separation, replacement and foundation.

Zermelo set theory

The usual set theory with extensionality, empty set, pairing, union, power set, infinity and full separation, before adjoining replacement. Modern presentations often include foundation; the convention should be specified when comparing theories. Class-theoretic variants add classes and class comprehension, rather than treating proper classes as sets.

Axiom of limitation of size

Every proper class is in bijection with the universe. Over class-theoretic Zermelo set theory, with class-parameter separation, this is equivalent to replacement plus global choice. For replacement, a proper functional image of a set would give a surjection from that set onto the universe, contradicted by diagonal separation. The proper class of ordinals supplies the global well-order. Conversely rank followed by uniformly chosen rank-segment well-orders is set-like, and every proper class in that order has order type equal to the entire ordinal class.

Intuitionistic Zermelo–Fraenkel set theory ( $IZF$ )

Full intuitionistic Zermelo–Fraenkel set theory uses intuitionistic first-order logic, extensionality, pairing, union, infinity, full separation, power set, collection and epsilon induction. Collection is stronger than replacement intuitionistically. This is distinct from predicative constructive ZF, which restricts separation and replaces full power set. The full theory supports a Boolean-valued inner universe over intuitionistic set theory, giving the relative consistency of classical ZF.

Boolean-valued inner universe over intuitionistic set theory ( $V^{B}$ )

Using the double-negation Boolean algebra, form well-founded names whose immediate subnames have truth-value weights. Define valued membership and equality by recursion on the underlying well-founded trees. Logical conjunction and universal quantification use meets; disjunction and existence use Boolean joins. Explicit names for pairs, unions and subsets verify the elementary set axioms, and collection for Boolean-valued names handles unbounded witnesses. The resulting internal valued universe validates classical ZF. This is a negative inner interpretation, not an assertion that the external intuitionistic universe satisfies excluded middle.

Boolean-valued name ( $a : dom (a) ⟶ B$ )

A well-founded recursively built set code with a set of immediate subnames and a Boolean coefficient for each. The coefficient records the extent to which the corresponding subname belongs. More generally one may permit repeated coded subnames, joining their coefficients. Recursive valued equality identifies different codes representing the same valued set; external equality of codes is not the interpreted equality.

Collection for Boolean-valued names

For a name

a

and formula

φ

, form the set of pairs

(u, p)

with

u

in the immediate domain of

a

p

a Boolean truth value, and some name

v

satisfying

p \leq a (u) \land [[φ (u, v)]]

. Full separation makes this a set, and intuitionistic collection gives a set of witness names covering all its pairs. A name with these witnesses in its domain collects the entire Boolean value of every existential assertion over

a

, without selecting one witness whose value is top. No choice or maximum principle is used.

Rieger-Bernays permutation model ( $x E y ⟺ x \in π (y)$ )

A definable class bijection

π

of a model's universe changes membership as displayed. Images and inverse images of sets under

π

remain sets by the Axiom schema of replacement. The new extension of

y

is the old set

π (y)

. Thus the representative of any desired extension

b

π^{- 1} (b)

. Extensionality follows from bijectivity; separation and replacement translate to old definable formulas; pairs, unions and power sets have explicit representatives. Infinity follows by iterating the new empty set and successor. Foundation need not survive: interchanging

\emptyset

and

{\emptyset}

makes the old empty set a Quine atom. A full such permutation of a model of choice still satisfies choice; failure of choice requires an additional symmetry restriction.

Quine atom ( $q = {q}$ )

A Quine atom is a set whose sole member is itself. It violates the Axiom of foundation while respecting the axiom of extensionality. Swapping pairwise distinct old objects

a_{n}

with their singletons in a Rieger-Bernays permutation model supplies many Quine atoms, provided those transpositions have disjoint supports. For example, the old ordinals

a_{n} = ω + n

and their singletons are disjoint families.

Extensional cumulative universe over Quine atoms

Start with distinct formal atoms

q \in A

with membership extensions

{q}

. Recursively adjoin a unique representative

S (X)

of every subset

X

of a previous stage, except that

S ({q}) = q

uses the atom already present. Define membership by these extensions. Each set-sized collection of objects has bounded construction rank, so it has a representative at a later stage. This gives full extensionality, unlike adjoining an ordinary singleton distinct from a Quine atom. Definable subsets and ranges, unions and power sets are set-sized collections in the ambient model and hence have representatives. The pure finite hierarchy supplies infinity. Every permutation of the atoms extends recursively; hereditary finite support restriction gives the hereditarily finite-supported Quine-atom model, whose two-element atom subsets have no choice function.

Hereditarily finite-supported Quine-atom model

Build the cumulative universe over an infinite set

A

of Quine atoms, and extend every permutation of

A

recursively to its other sets. An object has finite support if every permutation fixing that finite subset of

A

fixes the object. Retain objects whose members, recursively away from the atomic self-loops, also have finite support. Parameters and domains give finite supports for definable subsets and functional ranges; the collection of all retained subsets of a retained set is again supported. These observations verify separation, replacement and power set, and the pure natural-number hierarchy gives infinity. There is no choice function on the two-element subsets of

A

: swap two atoms outside its supposed finite support, fixing their unordered pair but interchanging either possible selected member.

Axiom of infinity

The axiom asserts the existence of a set containing the empty set and closed under the successor operation

x \mapsto x \cup {x}

\exists I (\emptyset \in I \land \forall x \in I (x \cup {x} \in I)) .

In Zermelo–Fraenkel set theory, this supplies a set from which the set of natural numbers is constructed.

Inductive set ( $\emptyset \in I \land \forall x \in I (x \cup {x} \in I)$ )

A set

I

is inductive if it contains the empty set and contains

x \cup {x}

whenever it contains

x

. The axiom of infinity asserts that an inductive set exists. The natural numbers form the least inductive set: intersect one inductive set with the class of objects belonging to every inductive set. This use of separation gives a set, and the defining class is closed under successor.

Zermelo–Fraenkel set theory with choice

ZFC is Zermelo–Fraenkel set theory together with the axiom of choice.

Von Neumann hierarchy ( $V_{α}$ )

The von Neumann hierarchy is

V_{0} = \emptyset, V_{α + 1} = P (V_{α}), V_{λ} = ⋃_{β < λ} V_{β} .

Every level is transitive, the levels are increasing, and every set belongs to some level.

Countable rank-initial segment cannot model ZFC

α

is a countable ordinal and

V_{α} ⊨ ZFC

, then

α

must be a limit ordinal. Choose a countable cofinal sequence

(α_{n})

α

. The internal axiom of choice gives, for every

n

, a bijection between

V_{α_{n}}

and some ordinal below

α

; that ordinal is externally countable, so every

V_{α_{n}}

is countable. Hence

V_{α} = ⋃_{n} V_{α_{n}}

is countable. But

V_{α}

contains the full power set

P (ω)

, which is uncountable by Cantor theorem, a contradiction.

Lévy reflection theorem

For every finite collection

Φ

of first-order formulas, there are arbitrarily large ordinals

α

such that, for every

φ \in Φ

and all parameters in

V_{α}

V_{α} ⊨ φ ⟺ V ⊨ φ .

The reflecting ordinals for

Φ

form a closed unbounded class.

Club reflection below an inaccessible cardinal

For inaccessible

κ

and any predicate

R \subseteq V_{κ}

, the ordinals

α < κ

with

⟨ V_{α}, \in, R \cap V_{α} ⟩ ≺ ⟨ V_{κ}, \in, R ⟩

form a club. Closure under ranks of existential witnesses gives unboundedness, and the elementary chain theorem gives closedness.

Reflection theorem for definable hierarchies

A finite collection of first-order formulas has a closed unbounded class of ordinals whose levels in a definable continuous hierarchy agree with its union for all parameters in the level. Close the collection under subformulas, bound the least witness levels for existential instances on each set-sized stage by Axiom schema of replacement, and iterate these bounds countably. Continuity supplies the closed stages, and induction on formulas proves agreement. The Tarski-Vaught test describes the same witness criterion. For a hierarchy of length an uncountable regular cardinal, bounds stay below that cardinal when every stage has smaller cardinality.

Ordinal described by a first-order formula

A first-order formula

φ

describes an ordinal

α

when

α

is the least ordinal such that

V_{α} ⊨ φ

. No strongly inaccessible cardinal can be described: if

V_{κ} ⊨ φ

, the Lévy reflection theorem produces some

α < κ

with

V_{α} ⊨ φ

Rank of a set

The rank is defined by

rank (x) = sup_{y \in x} (rank (y) + 1) .

It is the least ordinal

α

for which

x \subseteq V_{α}

Definable power set ( $D (X)$ )

The definable power set

D (X) = Def (X)

consists of the subsets of

X

definable over the first-order structure

(X, \in)

by a first-order formula with parameters from

X

. Satisfaction for a set structure makes this a definable operation in ZF. Iterating it produces the constructible hierarchy and the relative constructible hierarchy; their unions are the constructible universe and the relative constructible universe.

Finite relation closure for set-theoretic coding

A useful finite conjunction of closure assertions requires empty set, pairing, set union, set difference, Cartesian products, all finite tuple domains

A^{n}

, and the following operations on their relations: relative complements, intersections, coordinate projections and pullbacks along finite coordinate maps, together with equality and membership restricted to

A^{2}

. The arities and maps are quantified objects, so these requirements form finitely many first-order formulas, not an infinite schema. In a transitive set, individual finite tuples exist by pairing and union, making the tuple-domain assertions correct externally. Atomic truth relations, Boolean operations and projection then compute the truth table of each coded first-order formula correctly by finite induction. Thus satisfaction for a set structure and the relation

B = Def (A)

are absolute for shared arguments. Every nonzero limit level of the relative constructible hierarchy is closed under these operations, since each result can be defined at finitely many subsequent stages.

Constructible hierarchy ( $L_{α}$ )

The constructible hierarchy is defined by

L_{0} = \emptyset, L_{α + 1} = D (L_{α}), L_{λ} = ⋃_{α < λ} L_{α}

for limit ordinals

λ

. Its union is the constructible universe

L

Constructible sets of low rank can appear at later stages ( $L \cap V_{ω + 1} \neq = L_{ω + 1}$ )

The equality

L \cap V_{α} = L_{α}

can fail even at

α = ω + 1

. Inside the constructible universe,

L_{ω} = V_{ω}

is countable, so its definable power set

L_{ω + 1}

is countable. The constructible power set of

ω

is uncountable there by the Cantor theorem. A real outside

L_{ω + 1}

remains a constructible subset of

ω

, hence belongs to

V_{ω + 1}

. The cardinal comparison must be made inside

L

, since its reals can be externally countable.

Absoluteness of constructible levels ( $L_{α}^{M} = L_{α}$ )

For a transitive model

M

of ZFC and

α \in M \cap Ord

, the internally computed constructible hierarchy agrees with the ambient level:

L_{α}^{M} = L_{α}

. Satisfaction for a fixed set structure is computed from the same finite formulas and the same domain in both universes. Transfinite recursion then proves agreement at successors and limits. If

θ = M \cap Ord

, it follows that

L_{θ} \subseteq M

Constructible-level absoluteness over ZF ( $L_{α}^{M} = L_{α}$ )

M

is a transitive model of ZF, its internally computed

L_{α}

is the actual

L_{α}

for each ordinal

α \in M

. At a successor stage use absoluteness of satisfaction for the same set structure, formula codes and parameters; at a limit stage take the union of the already identical earlier stages. Choice is not required.

Constructible universe ( $L$ )

The constructible universe is the inner model

L = ⋃_{α \in Ord} L_{α}

obtained by iterating the definable power set. It satisfies ZFC and the Generalized continuum hypothesis.

Power-set axiom in the constructible universe ( $P^{L} (a) = P^{V} (a) \cap L \in L$ )

For

a \in L

, ambient separation forms

S = P (a) \cap L

. Ambient replacement bounds the first constructible stages of all members of

S

. At a stage containing

a

and all of

S

, the latter is definable by the bounded property of being a subset of

a

. Thus

S

belongs to the next constructible stage and is the internal power set in

L

Shepherdson's wall

The obstruction to proving the consistency of nonconstructibility by a uniform inner model construction is that, inside a universe satisfying

V = L

, every transitive inner model containing all ordinals has

L

as its own constructible universe and therefore is the entire ambient universe. The absoluteness of constructible levels proves this by induction over successor definability and limit unions. Thus a construction valid in every model of ZF cannot always produce such an inner model satisfying

V \neq = L

, and in particular cannot always produce one violating axiom of choice.

Axiom of constructibility ( $V = L$ )

Every set belongs to some level of the constructible hierarchy. The assertion is

\forall x \exists α (x \in L_{α})

, not that each set is definable without parameters. The constructible universe theorem supplies a relative-consistency model of this assertion from ZFC.

Separation proof in the constructible universe

To separate a subset of a constructible set by a formula interpreted in the constructible universe, apply the reflection theorem for definable hierarchies to the formula and its subformulas. At a sufficiently large reflecting level containing the parameters, the desired subset is definable and belongs to the next constructible hierarchy level. The reflection proof uses least witness stages and ambient Axiom schema of replacement, so does not presuppose Axiom schema of separation within the constructible universe.

Constructible universe theorem ( $L ⊨ ZFC + GCH$ )

ZFC proves that the constructible universe is an inner model of ZFC and satisfies the Generalized continuum hypothesis. Relativizing to

L

yields the corresponding relative-consistency implication.

Diamond theorem in the constructible universe ( $L ⊨ ♢$ )

The constructible universe satisfies the diamond principle. Together with antichain sealing by diamond, this supplies a Suslin tree in

L

Countability of constructible omega-one ( $NC : ∣ ω_{1}^{L} ∣ = ℵ_{0}$ )

This statement says that the first uncountable ordinal of an inner model

L

is a countable ordinal in the ambient universe. It can hold together with the Generalized continuum hypothesis: start with constructibility and use a finite-function collapse to countable size on

ω_{1}^{L}

. The GCH preservation by a finite-function collapse calculation gives the relative consistency result already from the consistency of ZFC.

Hereditarily countable constructible sets appear below omega-one ( $H_{ω_{1}}^{L} = L_{ω_{1}}^{L}$ )

Inside the constructible universe, every hereditarily countable set appears in a countable level of the constructible hierarchy. Take a countable elementary substructure of a sufficiently large

L_{η}

containing its transitive closure pointwise. The condensation lemma for the constructible universe identifies the collapse with

L_{β}

for countable

β

, and the collapse fixes the original set. Conversely, a countable-indexed level is countable inside the constructible universe.

Constructible power set ( $P^{L} (A)$ )

For

A \in L

, its constructible power set is

P^{L} (A) = {X \in L : X \subseteq A} = P (A) \cap L .

Unlike the single-stage definable power set

D (A)

, it includes subsets of

A

appearing arbitrarily late in the constructible hierarchy.

Ambient cardinal bound on the constructible reals ( $∣ P (ω) \cap L ∣ \leq ℵ_{1}$ )

In a ZFC universe, the constructible universe theorem supplies a bijection inside

L

between

ω_{1}^{L}

and its reals. The same graph is a bijection externally. Each ordinal below

ω_{1}^{L}

has a countability witness in

L

, hence also externally, proving

ω_{1}^{L} \leq ω_{1}

without assuming cardinal absoluteness. Therefore the constructible reals have ambient cardinality at most

ℵ_{1}

. If the ambient continuum is larger, some subset of

ω

is not constructible. The ordinal

ω_{1}^{L}

may be externally countable, so the argument is an upper bound and not a claim of equality.

Ambient constructible power sets when the reals are not well-orderable ( $a \in L ⟹ (P^{V} (a) \in L ⟺ a is finite)$ )

If the ambient power set of

ω

is not well-orderable and

a \in L

, then the full ambient power set of

a

belongs to

L

exactly when

a

is finite. Finite set operations give the forward construction for finite

a

. If

a

is infinite, its constructible well-order gives an injection

ω \to a

. The induced injection of power sets would make the ambient power set of

ω

well-orderable if

P (a)

belonged to

L

Relative constructible universe ( $L (A)$ )

For a transitive set

X

, the relative constructible universe

L (X)

is the union of the relative constructible hierarchy, starting at

L_{0} (X) = X

, applying the definable power set at successors and taking unions at limit ordinals. It is the smallest inner model of ZF containing

X

and all its members. For an arbitrary set

A

, take the base

X

to be the transitive closure of

{A}

, so that

A \in X

. Axiom of choice need not hold for an arbitrary base; the construction uses initial parameters rather than a predicate relativization.

Inner models with all reals preserve omega-one ( $ω_{1}^{W} = ω_{1}$ )

An inner model

W

of ZF containing all ambient subsets of

ω

computes the same countable ordinals as the ambient universe. Every ambient countably infinite ordinal has a well-order code coded by a subset of

ω

, hence that code belongs to

W

; finite ordinals are already shared. The Mostowski collapse theorem inside

W

recovers the actual ordinal and its countability witness. Conversely any countability witness in

W

remains one outside. If

W

also contains the full power set of

ω

as a set, its Continuum hypothesis would give an ambient bijection from

ω_{1}

onto that same power set. Thus an ambient failure of this well-orderable formulation of the Continuum hypothesis is preserved in such an inner model. No internal axiom of choice is required for this argument.

Relative constructible hierarchy ( $L_{α} (X)$ )

For a transitive set

X

, use

L_{0} (X) = X

L_{α + 1} (X) = Def (L_{α} (X))

and unions at nonzero limit ordinals. The successor operation is the definable power set. Each level is transitive and the levels increase; moreover

X \in L_{1} (X)

. Their union is

L (X)

, an inner model of ZF. The initial-set convention differs from a hierarchy using a predicate, or one starting at

X \cup {X}

. Axiom of choice need not hold for an arbitrary base without an internally available well-order.

Relative condensation lemma

α

is a nonzero limit ordinal and

Y ≺ L_{α} (X)

with

X \cup {X} \subseteq Y

, the Mostowski collapse theorem sends

Y

L_{β} (X)

for some nonzero limit

β \leq α

and fixes

X

pointwise. The base is fixed by transitivity and inclusion of all its members. Transfer the relative constructible level recognition formula first by elementarity and then through the collapse isomorphism to identify its image. If

ρ = X \cap Ord

, ordinal heights are

ρ + α

and

ρ + β

, giving the bound. Having only

X \in Y

does not guarantee this base-fixing version.

Relative constructible level recognition ( $M ⊨ Φ (X) ⟺ M = L_{α} (X)$ )

For transitive sets

M, X

with

X \in M

, a single first-order formula

Φ (X)

recognises the nonzero limit levels

L_{α} (X)

. Require finite relation closure for set-theoretic coding, transitivity of

X

, that every element belongs to a coded relative constructible stage, and that every represented stage index has a larger represented index. Correct history codes have downward-closed indices with no maximum, hence form a nonzero limit ordinal

α

. The exhaustion assertion and transitivity then give

M = ⋃_{ξ < α} L_{ξ} (X)

. Conversely every limit level has the required closure, correct histories cofinal in its index, and exhaustion. This formulation does not assume ZF for an arbitrary input

M

and does not replace finite coding closure with an unjustified internal constructibility assertion.

Coded relative constructible stage ( $S_{X} (ξ, B)$ )

This first-order formula asserts the existence of a history function on

ξ + 1

starting at

X

, applying definable power set at successors and unions at nonzero limit ordinals, and ending at

B

. In a transitive set satisfying finite relation closure for set-theoretic coding, each history is correct by transfinite induction, so

B = L_{ξ} (X)

. Relation operations produce restrictions to shorter histories. Since stage histories appear below every limit constructible level, every history of length

ξ + 1

for

ξ < α

belongs to

L_{α} (X)

when

α

is a nonzero limit ordinal. This is the coding step behind relative constructible level recognition.

Stage histories appear below every limit constructible level ( $f_{ξ} \in L_{α} (X) (ξ < α, α a nonzero limit)$ )

For a transitive set

X

, let

f_{ξ}

be the history function

η \mapsto L_{η} (X)

ξ + 1

in the relative constructible hierarchy. By transfinite induction,

f_{ξ} \in L_{ξ + k} (X)

for some finite

k

, possibly depending on

ξ

. The base and successor steps follow by forming finite ordered pairs and adjoining the next entry, using

L_{ξ + 1} (X) \in L_{ξ + 2} (X)

. These operations require finitely many subsequent definable power sets.

At a nonzero limit ordinal

λ

, the inductive bounds put every earlier

f_{η}

L_{λ} (X)

, since

η + k < λ

. This level satisfies finite relation closure for set-theoretic coding, independently of the availability of history functions. Consequently its coded relative constructible stage predicate computes the endpoints correctly. Finite pairing closure and the earlier histories show that

h = {⟨ η, B ⟩ \in L_{λ} (X) : (L_{λ} (X), \in) ⊨ S_{X} (η, B)}

contains exactly the pairs

⟨ η, L_{η} (X)⟩

for

η < λ

. There are no extra indices: if

η \geq λ

and

B = L_{η} (X) \in L_{λ} (X)

, increasing levels would give

B \in B

, contradicting Axiom of foundation. Thus

h = f_{λ} ↾ λ

is a definable subset of

L_{λ} (X)

and belongs to

L_{λ + 1} (X)

. Extracting its domain

λ

and adjoining

⟨ λ, L_{λ} (X)⟩

uses finitely many further operations, proving the induction step. Every nonzero limit

α

therefore contains all

f_{ξ}

with

ξ < α

, as required by relative constructible level recognition.

Relative constructible universe can violate the continuum hypothesis

Assume a transitive model

M

satisfies

2^{ℵ_{0}} = ℵ_{2}

. In

M

, encode a bijection

e : ω_{2} \to P (ω)

by one set

A \subseteq ω_{2}

, using a fixed pairing of

ω_{2} \times ω

with

ω_{2}

. Then

L (A)

decodes

e

and contains every real of

M

. The two models consequently have the same

ω_{1}

, and any bijection between

ω_{1}

and the real numbers in

L (A)

would also be one in

M

. Thus

L (A) ⊨ \neg CH

Condensation sentence for the constructible hierarchy

A condensation sentence is a fixed first-order sentence

σ

such that every transitive set satisfying

σ

L_{λ}

for a limit ordinal

λ

. It combines a sufficiently strong finite fragment of set theory, the assertion that every set is constructible, and the absence of a largest ordinal.

Well-order code

A well-order code is a binary relation

R \subseteq ω \times ω

for which

(ω, R)

is a well-order. Its representation is the unique countable ordinal isomorphic to

(ω, R)

Coding level of the constructible hierarchy

A level

L_{λ}

is a coding level when

λ

is a limit ordinal, the representation of every well-order code in

L_{λ}

is below

λ

, and every ordinal below

λ

has a well-order code in

L_{λ}

Condensation lemma for the constructible universe