Relative set theory: Strong stability by Karel Hrbacek (2012)

http://logicandanalysis.org/index.php/jla/article/view/158

Important Axioms:

theorem o (t : Type) (U V : Set t) : (∀ (x : t), x ∈ U ↔ x ∈ V) → U = V

Relativization o

theorem i (t : Type) (x : t) : ∃ (V : Set t), x ∈ V ∧ ∀ (U : Set t), x ∈ U → V ⊆ U

i

theorem ii : ∃ (t : Type), ¬∀ (V : Set (Set t)), ∅ ∈ V ∧ ∃ x ∈ V, ∀ (U : Set (Set t)), x ∈ U → V ⊆ U

ii

theorem iii : ∃ (t : Type), ¬∀ (U V : Set t), U ⊆ V ∨ V ⊆ U

iii

theorem iv (t : Type) : ¬∀ (U : Set t), ∃ (V : Set t), U ⊂ V

iv

theorem v (t : Type) (a : t) : ¬∀ (U V : Set t), U ⊂ V → ∃ (W : Set t), U ⊂ W ∧ W ⊂ V

v

def one (t : Type) (L : Set t) (V : t → Set t) : Prop

A set L is a level set if for all x,y is an element of L V(x) = V(y) implies x = y. Level sets are finite, and the relation v defined on L by x ⊑ y $ V(x) ⊆ V(y) is a wellordering. We always describe level sets in the increasing order by ⊑, if L = {z₀; z₁; ... ; zₗ} is a level set, then V(z₀) ⊂ V(z₁) ⊂ ... ⊂ V(zₗ).

Equations

• one t L V = ∀ x ∈ L, ∀ y ∈ L, V x = V y → x = y

def two (t : Type) (L V₀ V₁ : Set t) (V : t → Set t) : Prop

Let L be a level set. We write V ≅_L V' if V ⊆ V(z) <-> V' ⊆ V(z) and V(z) ⊆ V <-> V(z) ⊆ V' hold for all z elements of L. Either V = V₀ = V(z₀) for some j ≤ l, or V, V' ⊂ V(z₀), or V(zⱼ) ⊂ V, V' ⊂ V(zⱼ₊₁) for some j < l, or V(zₗ) ⊂ V; V' Therefore ≅_L classifies all levels into 2l + 3 classes

Equations

• two t L V₀ V₁ V = ∀ z ∈ L, (V₀ ⊆ V z ↔ V₁ ⊆ V z) ∧ (V z ⊆ V₀ ↔ V z ⊆ V₁)

theorem twoholdsifsame (t : Type) (L V₀ : Set t) (V : t → Set t) : two t L V₀ V₀ V