TauLib.Sets.Universe

τ-Universe properties: countability, no Russell set, no infinite descent.

Registry Cross-References

• [I.P13a] Countability — tau_idx_countable

• [I.P13b] No Russell Set — no_russell_set

• [I.P13c] No Infinite Descent — from tau_strict_mem_wf

Ground Truth Sources

• chunk_0365_M003070: Universe properties of τ-arithmetic sets

Mathematical Content

τ as class: τ is a proper class (a category), not a set. “x ∈ τ” means x is an object of the category — class membership, not set membership. The internal set theory developed here lives INSIDE τ, encoded arithmetically on the α-orbit O_α ≅ ℕ⁺.

The τ-set universe (= O_α = ℕ⁺) has three fundamental properties that distinguish it from naive set theory while maintaining computational power:

• Countability: TauIdx ≅ ℕ⁺, so the universe is trivially countable. The identity function witnesses the bijection.

• No Russell Set: There is no τ-set R such that for all a, a ∈_τ R iff a ∉_τ R. This follows from reflexivity of τ-membership (every a ∈_τ a since a | a), which means the “diagonal” argument produces a contradiction at a = R.

• No Infinite Descent: From well-foundedness of strict τ-membership (Powerset.lean), there is no infinite descending chain of nonzero strict τ-members. This is the τ-analogue of the Foundation Axiom.

Tau.Sets.tau_idx_is_nat

source theorem Tau.Sets.tau_idx_is_nat :Denotation.TauIdx = ℕ

The τ-index universe is Nat itself (by definition).

Tau.Sets.tau_idx_countable

source theorem Tau.Sets.tau_idx_countable :∃ (f : Denotation.TauIdx → ℕ), Function.Injective f

[I.P13a] The τ-set universe is countable: the identity function is a bijection TauIdx → Nat.

Tau.Sets.tau_idx_surjective

source theorem Tau.Sets.tau_idx_surjective (n : ℕ) :∃ (a : Denotation.TauIdx), a = n

The identity surjects onto Nat (universe is exactly Nat).

Tau.Sets.no_russell_set

source theorem Tau.Sets.no_russell_set :¬∃ (R : Denotation.TauIdx), ∀ (a : Denotation.TauIdx), tau_mem a R ↔ ¬tau_mem a R

[I.P13b] No Russell Set: there is no τ-set R such that for all a, a ∈_τ R iff ¬(a ∈_τ R).

Proof by contradiction: if such R existed, then applying the biconditional to a = R gives R ∈_τ R ↔ ¬(R ∈_τ R). But R ∈_τ R always holds (since R | R), so we get True ↔ False, a contradiction.

Tau.Sets.no_complement_of_self_mem

source theorem Tau.Sets.no_complement_of_self_mem :¬∃ (C : Denotation.TauIdx), ∀ (a : Denotation.TauIdx), tau_mem a C ↔ ¬tau_mem a a

Variant: no τ-set separates members from non-members via complement. There is no τ-set C that contains exactly the non-self-members.

Tau.Sets.is_descending_chain

source def Tau.Sets.is_descending_chain (f : ℕ → Denotation.TauIdx) :Prop

A descending chain is a function f : Nat → TauIdx such that f(n+1) is a strict nonzero member of f(n) for all n. Equations

• Tau.Sets.is_descending_chain f = ∀ (n : ℕ), Tau.Sets.tau_strict_mem_nz (f (n + 1)) (f n) Instances For

Tau.Sets.no_infinite_descent

source theorem Tau.Sets.no_infinite_descent :¬∃ (f : ℕ → Denotation.TauIdx), is_descending_chain f

[I.P13c] No Infinite Descent: there is no infinite descending chain of strict τ-membership through nonzero elements.

Proof: from well-foundedness of tau_strict_mem_nz. An infinite descending chain would contradict the well-foundedness of the relation, since it would produce a sequence with no minimal element.

Tau.Sets.tau_mem_preorder

source theorem Tau.Sets.tau_mem_preorder :(∀ (a : Denotation.TauIdx), tau_mem a a) ∧ ∀ (a b c : Denotation.TauIdx), tau_mem a b → tau_mem b c → tau_mem a c

The τ-universe is a preorder (reflexive + transitive membership).

Tau.Sets.tau_mem_partial_order

source theorem Tau.Sets.tau_mem_partial_order :(∀ (a : Denotation.TauIdx), tau_mem a a) ∧ (∀ (a b : Denotation.TauIdx), tau_mem a b → tau_mem b a → a = b) ∧ ∀ (a b c : Denotation.TauIdx), tau_mem a b → tau_mem b c → tau_mem a c

The τ-universe is a partial order (preorder + antisymmetry).