Axioms of ZF except Replacement.

Main Definitions

• IsEmptyset describes an emptyset.
• IsSingleton describes a singleton.
• IsPair describes an unordered pair.
• IsOrderedPair describes an ordered pair.
• IsUnion describes a union.
• IsSeparation describes {x∈(bv n) : ϕ}. The placeholder for ϕ is fv 0.
• A FirstOrder.ZFC.ModelEmptyset is a class of models of Set Theory with an emptyset.
• A FirstOrder.ZFC.ModelPairing is a class of models of Set Theory with the pairing axiom.
• A FirstOrder.ZFC.ModelUnion is a class of models of Set Theory with the pairing axiom.
• A FirstOrder.ZFC.ModelInfinity is a class of models of Set Theory with the infinity axiom.
• A FirstOrder.ZFC.ModelComprehension is a class of models of Set Theory with the comprehension schema.

Main Statements

• Various basic propositions prove from the axioms are proved.
• ext_induction and int_induction prove the mathematical induction externally an dinternally.

Notations

• Definitions that begin with "int" are to make a formula that describe it. When it is without prime, use the initial free variables as place holders. When it is with prime, accept terms as place holders.
• Definitions that begin with "Ext" are propositions that describe it externally.

theorem FirstOrder.Language.Term.liftAt_zero {n m : ℕ} (t : LZFC.Term (ℕ ⊕ Fin n)) : liftAt 0 m t = t

Term.liftAt 0 m t = t for any term t.

theorem FirstOrder.Language.BoundedFormula.liftAt_zero {n m : ℕ} (ϕ : LZFC.BoundedFormula ℕ n) : liftAt 0 m ϕ = ϕ

liftAt 0 m ϕ = ϕ for any bounded formula ϕ.

theorem FirstOrder.ZFC.realize_fixedSnoc_makeTsN_1 {V : Type u} [ModelSets V] {n : ℕ} {s : ℕ → V} {xs : Fin n → V} {x : V} : (fun (k : ℕ) => Language.Term.realize (Sum.elim s (FixedSnoc.fixedSnoc xs x)) (Language.BoundedFormula.makeTsN ![bv'' n] k)) = Language.BoundedFormula.replaceInitialValues s ![x]

Specialization of makeTsN to a single bv'' n.

theorem FirstOrder.ZFC.realize_fixedSnoc_makeTsN_2 {V : Type u} [ModelSets V] {n : ℕ} {s : ℕ → V} {xs : Fin n → V} {t₁ t₂ : Language.LZFC.Term (ℕ ⊕ Fin n)} : (fun (k : ℕ) => Language.Term.realize (Sum.elim s xs) (Language.BoundedFormula.makeTsN ![t₁, t₂] k)) = Language.BoundedFormula.replaceInitialValues s ![Language.Term.realize (Sum.elim s xs) t₁, Language.Term.realize (Sum.elim s xs) t₂]

Specialization of makeTsN to two arbitrary terms t₁, t₂.

theorem FirstOrder.ZFC.realize_fixedSnoc_makeTsN_3 {V : Type u} [ModelSets V] {n : ℕ} {s : ℕ → V} {xs : Fin n → V} {a b c : V} : (fun (k : ℕ) => Language.Term.realize (Sum.elim s (FixedSnoc.fixedSnoc (FixedSnoc.fixedSnoc (FixedSnoc.fixedSnoc xs a) b) c)) (Language.BoundedFormula.makeTsN ![bv'' n, bv'' (n + 1)] k)) = Language.BoundedFormula.replaceInitialValues s ![a, b]

Specialization of makeTsN to ![bv'' n, bv'' (n+1)] with three snocs.

theorem FirstOrder.ZFC.realize_fixedSnoc_makeTsN {V : Type u} [ModelSets V] {n m : ℕ} {s : ℕ → V} {xs : Fin n → V} {ts : Fin (m + 1) → Language.LZFC.Term (ℕ ⊕ Fin n)} : (fun (k : ℕ) => Language.Term.realize (Sum.elim s xs) (Language.BoundedFormula.makeTsN ts k)) = Language.BoundedFormula.replaceInitialValues s fun (i : Fin (m + 1)) => Language.Term.realize (Sum.elim s xs) (Language.BoundedFormula.makeTsN ts ↑i)

General makeTsN realization in terms of replaceInitialValues.

theorem FirstOrder.ZFC.Term.realize_fixedSnoc_0 {V : Type u} [ModelSets V] {n : ℕ} {s : ℕ → V} {xs : Fin n → V} {a b : V} : (fun (k : ℕ) => Language.Term.realize (Sum.elim s (FixedSnoc.fixedSnoc (FixedSnoc.fixedSnoc xs a) b)) (if k = 0 then bv'' n else Language.var (Sum.inl k))) = Language.BoundedFormula.replaceInitialValues s ![a]

Realization of a conditional bv'' term across two snocs collapses to replaceInitialValues s ![a].

def FirstOrder.ZFC.intIsEmptyset {n : ℕ} : Language.LZFC.BoundedFormula ℕ n

Describe that fv 0 is an emptyset.

Equations

• FirstOrder.ZFC.intIsEmptyset = (FirstOrder.ZFC.ϕnotElt (FirstOrder.ZFC.bv'' n) (FirstOrder.ZFC.fv' 0)).all

def FirstOrder.ZFC.intIsEmptyset' {n : ℕ} (t : Language.LZFC.Term (ℕ ⊕ Fin n)) : Language.LZFC.BoundedFormula ℕ n

Describe tht the given term is an emptyset.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.ZFC.ExtIsEmptyset {V : Type u} [ModelSets V] (a : V) : Prop

Describe a is an emptyset.

Equations

• FirstOrder.ZFC.ExtIsEmptyset a = ∀ (x : V), x ∉ a

class FirstOrder.ZFC.ModelEmptyset (V : Type u) extends FirstOrder.ZFC.ModelSets V : Type u

Model of Set Theory with an emptyset.

• funMap {n : ℕ} : LZFC.Functions n → (Fin n → V) → V
• RelMap {n : ℕ} : LZFC.Relations n → (Fin n → V) → Prop
• default : V
• isEltOf : V → V → Prop
• interpret_is_elt_of {a b : V} : a ∈ b ↔ Language.Structure.RelMap isEltOfTwo ![a, b]
• extensionality {a b : V} : (∀ (z : V), z ∈ a ↔ z ∈ b) → a = b
• emptyset_exists {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : (intIsEmptyset' (bv' 0)).ex.Realize s xs

  The model satisfies the existence of an emptyset.

theorem FirstOrder.ZFC.realize_is_emptyset {V : Type u} [ModelEmptyset V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (a : V) : intIsEmptyset.Realize (Language.BoundedFormula.replaceInitialValues s ![a]) xs ↔ ExtIsEmptyset a

@[simp]

theorem FirstOrder.ZFC.realize_is_emptyset' {V : Type u} [ModelEmptyset V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : intIsEmptyset.Realize s xs ↔ ExtIsEmptyset (s 0)

@[simp]

theorem FirstOrder.ZFC.realize_is_emptyset'' {V : Type u} [ModelEmptyset V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (t : Language.LZFC.Term (ℕ ⊕ Fin n)) : (intIsEmptyset' t).Realize s xs ↔ ExtIsEmptyset (Language.Term.realize (Sum.elim s xs) t)

theorem FirstOrder.ZFC.ext_emptyset_exists {V : Type u} [ModelEmptyset V] : ∃ (emp : V), ExtIsEmptyset emp

The emptyset exists.

theorem FirstOrder.ZFC.ext_emptyset_unique {V : Type u} [ModelEmptyset V] {a b : V} : ExtIsEmptyset a → ExtIsEmptyset b → a = b

The emptyset is unique.

theorem FirstOrder.ZFC.int_emptyset_unique {V : Type u} [ModelEmptyset V] {n : ℕ} {s : ℕ → V} {xs : Fin n → V} : ((intIsEmptyset' (bv' 0)).imp ((intIsEmptyset' (bv' 1)).imp ((bv' 0).bdEqual (bv' 1)))).all.all.Realize s xs

The emptyset is unique internally.

def FirstOrder.ZFC.intIsSingleton {n : ℕ} : Language.LZFC.BoundedFormula ℕ n

Describe fv 1 is a singleton of fv 0.

Equations

• FirstOrder.ZFC.intIsSingleton = ((FirstOrder.ZFC.ϕelt (FirstOrder.ZFC.bv'' n) (FirstOrder.ZFC.fv' 1)).iff ((FirstOrder.ZFC.bv'' n).bdEqual (FirstOrder.ZFC.fv (n + 1) 0))).all

def FirstOrder.ZFC.intIsPair {n : ℕ} : Language.LZFC.BoundedFormula ℕ n

Describe fv 2 is an unordered pair of fv 0 and fv 1.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.ZFC.intIsSingleton' {n : ℕ} (t₁ t₂ : Language.LZFC.Term (ℕ ⊕ Fin n)) : Language.LZFC.BoundedFormula ℕ n

Describe t₂ is a singleton of t₁.

Equations

• FirstOrder.ZFC.intIsSingleton' t₁ t₂ = FirstOrder.ZFC.intIsSingleton.replaceFV (FirstOrder.Language.BoundedFormula.makeTsN ![t₁, t₂])

def FirstOrder.ZFC.intIsPair' {n : ℕ} (t₁ t₂ t₃ : Language.LZFC.Term (ℕ ⊕ Fin n)) : Language.LZFC.BoundedFormula ℕ n

Describe t₃ is an unordered pair of t₁ and t₂.

Equations

• FirstOrder.ZFC.intIsPair' t₁ t₂ t₃ = FirstOrder.ZFC.intIsPair.replaceFV (FirstOrder.Language.BoundedFormula.makeTsN ![t₁, t₂, t₃])

class FirstOrder.ZFC.ModelPairing (V : Type u) extends FirstOrder.ZFC.ModelSets V : Type u

Model with a pairing axiom.

• funMap {n : ℕ} : LZFC.Functions n → (Fin n → V) → V
• RelMap {n : ℕ} : LZFC.Relations n → (Fin n → V) → Prop
• default : V
• isEltOf : V → V → Prop
• interpret_is_elt_of {a b : V} : a ∈ b ↔ Language.Structure.RelMap isEltOfTwo ![a, b]
• extensionality {a b : V} : (∀ (z : V), z ∈ a ↔ z ∈ b) → a = b
• pairing (s : ℕ → V) (xs : Fin 0 → V) : (intIsPair.liftAndReplaceFV 3 0 ![bv 3 0, bv 3 1, bv 3 2]).ex.all.all.Realize s xs

  The model satisfies the pairing axiom.

def FirstOrder.ZFC.ExtIsSingleton {V : Type u} [ModelPairing V] (a b : V) : Prop

Describe b is a singleton of a.

Equations

• FirstOrder.ZFC.ExtIsSingleton a b = ∀ (x : V), x ∈ b ↔ x = a

def FirstOrder.ZFC.ExtIsPair {V : Type u} [ModelPairing V] (a b c : V) : Prop

Describe c is an unordered pair of a and b.

Equations

• FirstOrder.ZFC.ExtIsPair a b c = ∀ (x : V), x ∈ c ↔ x = a ∨ x = b

@[simp]

theorem FirstOrder.ZFC.realize_is_singleton {V : Type u} [ModelPairing V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : intIsSingleton.Realize s xs ↔ ExtIsSingleton (s 0) (s 1)

@[simp]

theorem FirstOrder.ZFC.realize_is_singleton' {V : Type u} [ModelPairing V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (t₁ t₂ : Language.LZFC.Term (ℕ ⊕ Fin n)) : (intIsSingleton' t₁ t₂).Realize s xs ↔ ExtIsSingleton (Language.Term.realize (Sum.elim s xs) t₁) (Language.Term.realize (Sum.elim s xs) t₂)

@[simp]

theorem FirstOrder.ZFC.realize_is_pair {V : Type u} [ModelPairing V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : intIsPair.Realize s xs ↔ ExtIsPair (s 0) (s 1) (s 2)

theorem FirstOrder.ZFC.ext_pairing {V : Type u} [ModelPairing V] (a b : V) : ∃ (c : V), ExtIsPair a b c

Pairing Axiom described externally.

theorem FirstOrder.ZFC.ext_singleton_unique {V : Type u} [ModelPairing V] {a b b' : V} : ExtIsSingleton a b → ExtIsSingleton a b' → b = b'

The singleton is unique.

theorem FirstOrder.ZFC.ext_singleton_inj {V : Type u} [ModelPairing V] {a a' b : V} : ExtIsSingleton a b → ExtIsSingleton a' b → a = a'

{a} = {b} implies a = b.

theorem FirstOrder.ZFC.singleton_by_pair {V : Type u} [ModelPairing V] {a b : V} : ExtIsSingleton a b ↔ ExtIsPair a a b

{a, a} = {a}.

theorem FirstOrder.ZFC.ext_pair_unique {V : Type u} [ModelPairing V] {a b c c' : V} : ExtIsPair a b c → ExtIsPair a b c' → c = c'

The unordered pair is unique.

theorem FirstOrder.ZFC.ext_pairing_inj {V : Type u} [ModelPairing V] {a b a' b' c : V} : ExtIsPair a b c → ExtIsPair a' b' c → a = a' ∧ b = b' ∨ a = b' ∧ b = a'

Pairing is injective up to ordering.

theorem FirstOrder.ZFC.ext_singleton {V : Type u} [ModelPairing V] (a : V) : ∃ (b : V), ExtIsSingleton a b

Every element has a singleton.

theorem FirstOrder.ZFC.singleton_eq_pair {V : Type u} [ModelPairing V] {a b c x : V} : ExtIsSingleton a x → ExtIsPair b c x → a = b ∧ a = c

{a} = {b, c} implies a=b=c.

def FirstOrder.ZFC.intIsOrderedPair {n : ℕ} : Language.LZFC.BoundedFormula ℕ n

Describe fv 2 is an ordered pair of fv 0 and fv 1.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.ZFC.ExtIsOrderedPair {V : Type u} [ModelPairing V] (a b c : V) : Prop

Describe c is an ordered pair of a and b.

Equations

• FirstOrder.ZFC.ExtIsOrderedPair a b c = ∀ (x : V), x ∈ c ↔ FirstOrder.ZFC.ExtIsSingleton a x ∨ FirstOrder.ZFC.ExtIsPair a b x

@[simp]

theorem FirstOrder.ZFC.realize_is_ordered_pair {V : Type u} [ModelPairing V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : intIsOrderedPair.Realize s xs ↔ ExtIsOrderedPair (s 0) (s 1) (s 2)

theorem FirstOrder.ZFC.ext_ordered_pair {V : Type u} [ModelPairing V] (a b : V) : ∃ (c : V), ExtIsOrderedPair a b c

The ordered pair exists.

theorem FirstOrder.ZFC.ext_ordered_pair_unique {V : Type u} [ModelPairing V] (a b c c' : V) : ExtIsOrderedPair a b c → ExtIsOrderedPair a b c' → c = c'

The ordered pair is unique.

theorem FirstOrder.ZFC.ext_ordered_pair_inj {V : Type u} [ModelPairing V] (a b a' b' c : V) : ExtIsOrderedPair a b c → ExtIsOrderedPair a' b' c → a = a' ∧ b = b'

The ordered pair is injective.

theorem FirstOrder.ZFC.int_ordered_pair_inj {V : Type u} [ModelPairing V] (s : ℕ → V) (xs : Fin 0 → V) : ((intIsOrderedPair.liftAndReplaceFV 5 0 ![bv 5 0, bv 5 1, bv 5 4]).imp ((intIsOrderedPair.liftAndReplaceFV 5 0 ![bv 5 2, bv 5 3, bv 5 4]).imp ((bv 5 0).bdEqual (bv 5 2)∧'(bv 5 1).bdEqual (bv 5 3)))).all.all.all.all.all.Realize s xs

The ordered pair is injective internally.

class FirstOrder.ZFC.ModelEP (V : Type u) extends FirstOrder.ZFC.ModelEmptyset V, FirstOrder.ZFC.ModelPairing V : Type u

Model with both emptyset and pairing.

• funMap {n : ℕ} : LZFC.Functions n → (Fin n → V) → V
• RelMap {n : ℕ} : LZFC.Relations n → (Fin n → V) → Prop
• default : V
• isEltOf : V → V → Prop
• interpret_is_elt_of {a b : V} : a ∈ b ↔ Language.Structure.RelMap isEltOfTwo ![a, b]
• extensionality {a b : V} : (∀ (z : V), z ∈ a ↔ z ∈ b) → a = b
• emptyset_exists {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : (intIsEmptyset' (bv' 0)).ex.Realize s xs
• pairing (s : ℕ → V) (xs : Fin 0 → V) : (intIsPair.liftAndReplaceFV 3 0 ![bv 3 0, bv 3 1, bv 3 2]).ex.all.all.Realize s xs

theorem FirstOrder.ZFC.ext_singleton_of_emptyset {V : Type u} [ModelEP V] (e : V) : ExtIsEmptyset e → ∃ (a : V), ExtIsSingleton e a

A singleton can be formed for any emptyset element.

theorem FirstOrder.ZFC.int_singleton_of_emptyset {V : Type u} [ModelEP V] (s : ℕ → V) (xs : Fin 0 → V) : ((intIsEmptyset.liftAndReplaceFV 1 0 ![bv 1 0]).imp (intIsSingleton.liftAndReplaceFV 2 0 ![bv 2 0, bv 2 1]).ex).all.Realize s xs

A singleton can be formed for the emptyset internally.

def FirstOrder.ZFC.intIsUnion {n : ℕ} : Language.LZFC.BoundedFormula ℕ n

Describe fv 1 is the union of fv 0 (in the set-theoretic sense).

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.ZFC.intIsUnion' {n : ℕ} (t₁ t₂ : Language.LZFC.Term (ℕ ⊕ Fin n)) : Language.LZFC.BoundedFormula ℕ n

Describe t₂ is the union of t₁ (in the set-theoretic sense).

Equations

• FirstOrder.ZFC.intIsUnion' t₁ t₂ = FirstOrder.ZFC.intIsUnion.replaceFV (FirstOrder.Language.BoundedFormula.makeTsN ![t₁, t₂])

def FirstOrder.ZFC.ExtIsUnion {V : Type u} [ModelSets V] (a b : V) : Prop

Desdribe b is an union of a.

Equations

• FirstOrder.ZFC.ExtIsUnion a b = ∀ (x : V), x ∈ b ↔ ∃ (c : V), x ∈ c ∧ c ∈ a

class FirstOrder.ZFC.ModelUnion (V : Type u) extends FirstOrder.ZFC.ModelSets V : Type u

Model with the Union axiom.

• funMap {n : ℕ} : LZFC.Functions n → (Fin n → V) → V
• RelMap {n : ℕ} : LZFC.Relations n → (Fin n → V) → Prop
• default : V
• isEltOf : V → V → Prop
• interpret_is_elt_of {a b : V} : a ∈ b ↔ Language.Structure.RelMap isEltOfTwo ![a, b]
• extensionality {a b : V} : (∀ (z : V), z ∈ a ↔ z ∈ b) → a = b
• union_exists (s : ℕ → V) (xs : Fin 0 → V) : (intIsUnion.liftAndReplaceFV 2 0 ![bv' 0, bv' 1]).ex.all.Realize s xs

  The model satisfies the union axiom.

class FirstOrder.ZFC.ModelEPU (V : Type u) extends FirstOrder.ZFC.ModelEmptyset V, FirstOrder.ZFC.ModelPairing V, FirstOrder.ZFC.ModelUnion V : Type u

Model with emptyset, pairing, and union.

• funMap {n : ℕ} : LZFC.Functions n → (Fin n → V) → V
• RelMap {n : ℕ} : LZFC.Relations n → (Fin n → V) → Prop
• default : V
• isEltOf : V → V → Prop
• interpret_is_elt_of {a b : V} : a ∈ b ↔ Language.Structure.RelMap isEltOfTwo ![a, b]
• extensionality {a b : V} : (∀ (z : V), z ∈ a ↔ z ∈ b) → a = b
• emptyset_exists {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : (intIsEmptyset' (bv' 0)).ex.Realize s xs
• pairing (s : ℕ → V) (xs : Fin 0 → V) : (intIsPair.liftAndReplaceFV 3 0 ![bv 3 0, bv 3 1, bv 3 2]).ex.all.all.Realize s xs
• union_exists (s : ℕ → V) (xs : Fin 0 → V) : (intIsUnion.liftAndReplaceFV 2 0 ![bv' 0, bv' 1]).ex.all.Realize s xs

@[simp]

theorem FirstOrder.ZFC.realize_is_union {V : Type u} [ModelUnion V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : intIsUnion.Realize s xs ↔ ExtIsUnion (s 0) (s 1)

theorem FirstOrder.ZFC.union_of_ordered_pair {V : Type u} [ModelEPU V] {a b c d : V} : ExtIsOrderedPair a b c → ExtIsUnion c d → ExtIsPair a b d

The union of (a, b) equals {a, b}.

theorem FirstOrder.ZFC.int_union_of_ordered_pair {V : Type u} [ModelEPU V] {s : ℕ → V} {xs : Fin 0 → V} : ((intIsOrderedPair.liftAndReplaceFV 4 0 ![bv' 0, bv' 1, bv' 2]).imp ((intIsUnion.liftAndReplaceFV 4 0 ![bv' 2, bv' 3]).imp (intIsPair.liftAndReplaceFV 4 0 ![bv' 0, bv' 1, bv' 3]))).all.all.all.all.Realize s xs

The union of (a, b) equals {a, b} internally.

def FirstOrder.ZFC.intIsSubset {n : ℕ} : Language.LZFC.BoundedFormula ℕ n

Make a formula fv 0 ⊆ fv 1.

Equations

• FirstOrder.ZFC.intIsSubset = ((FirstOrder.ZFC.ϕelt (FirstOrder.ZFC.bv'' n) (FirstOrder.ZFC.fv (n + 1) 0)).imp (FirstOrder.ZFC.ϕelt (FirstOrder.ZFC.bv'' n) (FirstOrder.ZFC.fv (n + 1) 1))).all

def FirstOrder.ZFC.intIsSubset' {n : ℕ} (t₁ t₂ : Language.LZFC.Term (ℕ ⊕ Fin n)) : Language.LZFC.BoundedFormula ℕ n

Make a formula t1 ⊆ t2.

Equations

• t₁ ⊆' t₂ = FirstOrder.ZFC.intIsSubset.replaceFV (FirstOrder.Language.BoundedFormula.makeTsN ![t₁, t₂])

def FirstOrder.ZFC.«term_⊆'_» : Lean.TrailingParserDescr

Make a formula t1 ⊆ t2.

Equations

• FirstOrder.ZFC.«term_⊆'_» = Lean.ParserDescr.trailingNode `FirstOrder.ZFC.«term_⊆'_» 120 120 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊆' ") (Lean.ParserDescr.cat `term 121))

def FirstOrder.ZFC.intNotIsSubset' {n : ℕ} (t₁ t₂ : Language.LZFC.Term (ℕ ⊕ Fin n)) : Language.LZFC.BoundedFormula ℕ n

Make a formula t1 ⊈ t2.

Equations

• t₁ ⊈' t₂ = (t₁ ⊆' t₂).not

def FirstOrder.ZFC.«term_⊈'_» : Lean.TrailingParserDescr

Make a formula t1 ⊈ t2.

Equations

• FirstOrder.ZFC.«term_⊈'_» = Lean.ParserDescr.trailingNode `FirstOrder.ZFC.«term_⊈'_» 120 120 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊈' ") (Lean.ParserDescr.cat `term 121))

def FirstOrder.ZFC.ExtIsSubset {V : Type u} [ModelSets V] (a b : V) : Prop

a is a subset of b.

Equations

• FirstOrder.ZFC.ExtIsSubset a b = ∀ (x : V), x ∈ a → x ∈ b

def FirstOrder.ZFC.ExtNotIsSubset {V : Type u} [ModelSets V] (a b : V) : Prop

a is not a subset of b.

Equations

• (a ⊈ b) = ¬∀ (x : V), x ∈ a → x ∈ b

@[instance_reducible]

instance FirstOrder.ZFC.instHasSubsetOfModelSets {V : Type u} [ModelSets V] : HasSubset V

The ⊆ notation on a model of set theory is ExtIsSubset. This is an instance rather than a bare notation because a bare ⊆ notation is shadowed by the core one.

Equations

• FirstOrder.ZFC.instHasSubsetOfModelSets = { Subset := FirstOrder.ZFC.ExtIsSubset }

@[simp]

theorem FirstOrder.ZFC.subset_iff_extIsSubset {V : Type u} [ModelSets V] (a b : V) : a ⊆ b ↔ ExtIsSubset a b

def FirstOrder.ZFC.«term_⊈_» : Lean.TrailingParserDescr

a is not a subset of b.

Equations

• FirstOrder.ZFC.«term_⊈_» = Lean.ParserDescr.trailingNode `FirstOrder.ZFC.«term_⊈_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊈ ") (Lean.ParserDescr.cat `term 51))

def FirstOrder.ZFC.intIsPowerset {n : ℕ} : Language.LZFC.BoundedFormula ℕ n

Make a formula that fv 0 is a subset of fv 1.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.ZFC.intIsPowerset' {n : ℕ} (t₁ t₂ : Language.LZFC.Term (ℕ ⊕ Fin n)) : Language.LZFC.BoundedFormula ℕ n

Make a formula that t₂ is a powerset of t₁.

Equations

• FirstOrder.ZFC.intIsPowerset' t₁ t₂ = FirstOrder.ZFC.intIsPowerset.replaceFV (FirstOrder.Language.BoundedFormula.makeTsN ![t₁, t₂])

def FirstOrder.ZFC.ExtIsPowerset {V : Type u} [ModelSets V] (a b : V) : Prop

Describe b is a powerset of a.

Equations

• FirstOrder.ZFC.ExtIsPowerset a b = ∀ (x : V), FirstOrder.ZFC.ExtIsSubset x a ↔ x ∈ b

class FirstOrder.ZFC.ModelPowerset (V : Type u) extends FirstOrder.ZFC.ModelSets V : Type u

Model with the Powerset Axiom.

• funMap {n : ℕ} : LZFC.Functions n → (Fin n → V) → V
• RelMap {n : ℕ} : LZFC.Relations n → (Fin n → V) → Prop
• default : V
• isEltOf : V → V → Prop
• interpret_is_elt_of {a b : V} : a ∈ b ↔ Language.Structure.RelMap isEltOfTwo ![a, b]
• extensionality {a b : V} : (∀ (z : V), z ∈ a ↔ z ∈ b) → a = b
• powerset_exists (s : ℕ → V) (xs : Fin 0 → V) : (intIsPowerset.liftAndReplaceFV 2 0 ![bv 2 0, bv 2 1]).ex.all.Realize s xs

  The model satisfies the powerset axiom.

class FirstOrder.ZFC.ModelEPUP (V : Type u) extends FirstOrder.ZFC.ModelEmptyset V, FirstOrder.ZFC.ModelPairing V, FirstOrder.ZFC.ModelUnion V, FirstOrder.ZFC.ModelPowerset V : Type u

Model with emptyset, pairing, union, and powerset.

• funMap {n : ℕ} : LZFC.Functions n → (Fin n → V) → V
• RelMap {n : ℕ} : LZFC.Relations n → (Fin n → V) → Prop
• default : V
• isEltOf : V → V → Prop
• interpret_is_elt_of {a b : V} : a ∈ b ↔ Language.Structure.RelMap isEltOfTwo ![a, b]
• extensionality {a b : V} : (∀ (z : V), z ∈ a ↔ z ∈ b) → a = b
• emptyset_exists {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : (intIsEmptyset' (bv' 0)).ex.Realize s xs
• pairing (s : ℕ → V) (xs : Fin 0 → V) : (intIsPair.liftAndReplaceFV 3 0 ![bv 3 0, bv 3 1, bv 3 2]).ex.all.all.Realize s xs
• union_exists (s : ℕ → V) (xs : Fin 0 → V) : (intIsUnion.liftAndReplaceFV 2 0 ![bv' 0, bv' 1]).ex.all.Realize s xs
• powerset_exists (s : ℕ → V) (xs : Fin 0 → V) : (intIsPowerset.liftAndReplaceFV 2 0 ![bv 2 0, bv 2 1]).ex.all.Realize s xs

@[simp]

theorem FirstOrder.ZFC.realize_is_subset {V : Type u} [ModelPowerset V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : intIsSubset.Realize s xs ↔ ExtIsSubset (s 0) (s 1)

@[simp]

theorem FirstOrder.ZFC.realize_is_subset' {V : Type u} [ModelPowerset V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (t₁ t₂ : Language.LZFC.Term (ℕ ⊕ Fin n)) : (t₁ ⊆' t₂).Realize s xs ↔ ExtIsSubset (Language.Term.realize (Sum.elim s xs) t₁) (Language.Term.realize (Sum.elim s xs) t₂)

@[simp]

theorem FirstOrder.ZFC.realize_is_powerset {V : Type u} [ModelPowerset V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : intIsPowerset.Realize s xs ↔ ExtIsPowerset (s 0) (s 1)

@[simp]

theorem FirstOrder.ZFC.realize_is_powerset' {V : Type u} [ModelPowerset V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (t₁ t₂ : Language.LZFC.Term (ℕ ⊕ Fin n)) : (intIsPowerset' t₁ t₂).Realize s xs ↔ ExtIsPowerset (Language.Term.realize (Sum.elim s xs) t₁) (Language.Term.realize (Sum.elim s xs) t₂)

theorem FirstOrder.ZFC.subset_self {V : Type u} [ModelEPUP V] (a : V) : a ⊆ a

Every set is a subset of itself.

theorem FirstOrder.ZFC.int_subset_self {V : Type u} [ModelEPUP V] {s : ℕ → V} {xs : Fin 0 → V} : (bv 1 0 ⊆' bv 1 0).all.Realize s xs

Every set is a subset of itself internally.

theorem FirstOrder.ZFC.powerset_of_emptyset {V : Type u} [ModelEPUP V] (emp a : V) : ExtIsEmptyset emp → ExtIsPowerset emp a → ExtIsSingleton emp a

P(∅)={∅}

theorem FirstOrder.ZFC.int_powerset_of_emptyset {V : Type u} [ModelEPUP V] {s : ℕ → V} {xs : Fin 0 → V} : ((intIsEmptyset' (bv' 0)).imp ((intIsPowerset' (bv' 0) (bv' 1)).imp (intIsSingleton' (bv' 0) (bv' 1)))).all.all.Realize s xs

P(∅)={∅} internally.

def FirstOrder.ZFC.intIsSuccessor {n : ℕ} : Language.LZFC.BoundedFormula ℕ n

Make a formula for fv 1 is a successor of fv 0.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.ZFC.intIsSuccessor' {n : ℕ} (t₁ t₂ : Language.LZFC.Term (ℕ ⊕ Fin n)) : Language.LZFC.BoundedFormula ℕ n

Make a formula for t₂ is a successor of t₁-.

Equations

• FirstOrder.ZFC.intIsSuccessor' t₁ t₂ = FirstOrder.ZFC.intIsSuccessor.replaceFV (FirstOrder.Language.BoundedFormula.makeTsN ![t₁, t₂])

def FirstOrder.ZFC.ExtIsSuccessor {V : Type u} [ModelSets V] (a b : V) : Prop

Externally, b is a successor of a.

Equations

• FirstOrder.ZFC.ExtIsSuccessor a b = ∀ (x : V), x ∈ b ↔ x ∈ a ∨ x = a

@[simp]

theorem FirstOrder.ZFC.realize_is_successor {V : Type u} [ModelPowerset V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : intIsSuccessor.Realize s xs ↔ ExtIsSuccessor (s 0) (s 1)

@[simp]

theorem FirstOrder.ZFC.realize_is_successor' {V : Type u} [ModelPowerset V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (t₁ t₂ : Language.LZFC.Term (ℕ ⊕ Fin n)) : (intIsSuccessor' t₁ t₂).Realize s xs ↔ ExtIsSuccessor (Language.Term.realize (Sum.elim s xs) t₁) (Language.Term.realize (Sum.elim s xs) t₂)

def FirstOrder.ZFC.intIsInductive {n : ℕ} : Language.LZFC.BoundedFormula ℕ n

Make a formula for fv 0 is inductive, i.e., ∅∈fv 0 and x∈fv 0 implies S(x)∈fv 0.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.ZFC.intIsInductive' {n : ℕ} (t : Language.LZFC.Term (ℕ ⊕ Fin n)) : Language.LZFC.BoundedFormula ℕ n

Make a formula for t is inductive.

Equations

• FirstOrder.ZFC.intIsInductive' t = FirstOrder.ZFC.intIsInductive.replaceFV (FirstOrder.Language.BoundedFormula.makeTsN ![t])

def FirstOrder.ZFC.ExtIsInductive {V : Type u} [ModelEmptyset V] (a : V) : Prop

Describe a is inductive.

Equations

• FirstOrder.ZFC.ExtIsInductive a = ((∀ (emp : V), FirstOrder.ZFC.ExtIsEmptyset emp → emp ∈ a) ∧ ∀ (x : V), x ∈ a → ∀ (y : V), FirstOrder.ZFC.ExtIsSuccessor x y → y ∈ a)

@[simp]

theorem FirstOrder.ZFC.realize_is_inductive {V : Type u} [ModelEPUP V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : intIsInductive.Realize s xs ↔ ExtIsInductive (s 0)

@[simp]

theorem FirstOrder.ZFC.realize_is_inductive' {V : Type u} [ModelEPUP V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (t : Language.LZFC.Term (ℕ ⊕ Fin n)) : (intIsInductive' t).Realize s xs ↔ ExtIsInductive (Language.Term.realize (Sum.elim s xs) t)

theorem FirstOrder.ZFC.ext_emp_in_inductive {V : Type u} [ModelEPUP V] {emp a : V} : ExtIsEmptyset emp → ExtIsInductive a → emp ∈ a

∅ belongs to every inductive set.

theorem FirstOrder.ZFC.ext_inductive_one_step {V : Type u} [ModelEPUP V] {a y : V} (x : V) : ExtIsInductive a → x ∈ a → ExtIsSuccessor x y → y ∈ a

If a is inductive and x∈a, then S(x)∈a.

class FirstOrder.ZFC.ModelInfinity (V : Type u) extends FirstOrder.ZFC.ModelSets V : Type u

Model with the Infinity axiom.

• funMap {n : ℕ} : LZFC.Functions n → (Fin n → V) → V
• RelMap {n : ℕ} : LZFC.Relations n → (Fin n → V) → Prop
• default : V
• isEltOf : V → V → Prop
• interpret_is_elt_of {a b : V} : a ∈ b ↔ Language.Structure.RelMap isEltOfTwo ![a, b]
• extensionality {a b : V} : (∀ (z : V), z ∈ a ↔ z ∈ b) → a = b
• infinity_exists {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : (intIsInductive' (bv'' n)).ex.Realize s xs

  The model satisfies the existence of an inductive set.

class FirstOrder.ZFC.ModelEPUPI (V : Type u) extends FirstOrder.ZFC.ModelEPUP V, FirstOrder.ZFC.ModelInfinity V : Type u

Model with emptyset, pairing, union, powerset, and infinity.

• funMap {n : ℕ} : LZFC.Functions n → (Fin n → V) → V
• RelMap {n : ℕ} : LZFC.Relations n → (Fin n → V) → Prop
• default : V
• isEltOf : V → V → Prop
• interpret_is_elt_of {a b : V} : a ∈ b ↔ Language.Structure.RelMap isEltOfTwo ![a, b]
• extensionality {a b : V} : (∀ (z : V), z ∈ a ↔ z ∈ b) → a = b
• emptyset_exists {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : (intIsEmptyset' (bv' 0)).ex.Realize s xs
• pairing (s : ℕ → V) (xs : Fin 0 → V) : (intIsPair.liftAndReplaceFV 3 0 ![bv 3 0, bv 3 1, bv 3 2]).ex.all.all.Realize s xs
• union_exists (s : ℕ → V) (xs : Fin 0 → V) : (intIsUnion.liftAndReplaceFV 2 0 ![bv' 0, bv' 1]).ex.all.Realize s xs
• powerset_exists (s : ℕ → V) (xs : Fin 0 → V) : (intIsPowerset.liftAndReplaceFV 2 0 ![bv 2 0, bv 2 1]).ex.all.Realize s xs
• infinity_exists {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : (intIsInductive' (bv'' n)).ex.Realize s xs

theorem FirstOrder.ZFC.ext_infinity_exists {V : Type u} [ModelEPUPI V] : ∃ (x : V), ExtIsInductive x

The exitetence of an infinite set described externally.

def FirstOrder.ZFC.intRegularity {n : ℕ} : Language.LZFC.BoundedFormula ℕ n

Make a formula for the Regularity Axiom.

Equations

• One or more equations did not get rendered due to their size.

class FirstOrder.ZFC.ModelRegularity (V : Type u) extends FirstOrder.ZFC.ModelSets V : Type u

Model with the Regularity Axiom.

• funMap {n : ℕ} : LZFC.Functions n → (Fin n → V) → V
• RelMap {n : ℕ} : LZFC.Relations n → (Fin n → V) → Prop
• default : V
• isEltOf : V → V → Prop
• interpret_is_elt_of {a b : V} : a ∈ b ↔ Language.Structure.RelMap isEltOfTwo ![a, b]
• extensionality {a b : V} : (∀ (z : V), z ∈ a ↔ z ∈ b) → a = b
• regularity (s : ℕ → V) (xs : Fin 0 → V) : intRegularity.Realize s xs

  The model satisfies the regularity axiom.

class FirstOrder.ZFC.ModelEPUPIR (V : Type u) extends FirstOrder.ZFC.ModelEPUPI V, FirstOrder.ZFC.ModelRegularity V : Type u

Model with emptyset, pairing, union, powerset, infinity, and regularity.

• funMap {n : ℕ} : LZFC.Functions n → (Fin n → V) → V
• RelMap {n : ℕ} : LZFC.Relations n → (Fin n → V) → Prop
• default : V
• isEltOf : V → V → Prop
• interpret_is_elt_of {a b : V} : a ∈ b ↔ Language.Structure.RelMap isEltOfTwo ![a, b]
• extensionality {a b : V} : (∀ (z : V), z ∈ a ↔ z ∈ b) → a = b
• emptyset_exists {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : (intIsEmptyset' (bv' 0)).ex.Realize s xs
• pairing (s : ℕ → V) (xs : Fin 0 → V) : (intIsPair.liftAndReplaceFV 3 0 ![bv 3 0, bv 3 1, bv 3 2]).ex.all.all.Realize s xs
• union_exists (s : ℕ → V) (xs : Fin 0 → V) : (intIsUnion.liftAndReplaceFV 2 0 ![bv' 0, bv' 1]).ex.all.Realize s xs
• powerset_exists (s : ℕ → V) (xs : Fin 0 → V) : (intIsPowerset.liftAndReplaceFV 2 0 ![bv 2 0, bv 2 1]).ex.all.Realize s xs
• infinity_exists {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : (intIsInductive' (bv'' n)).ex.Realize s xs
• regularity (s : ℕ → V) (xs : Fin 0 → V) : intRegularity.Realize s xs

theorem FirstOrder.ZFC.ExtRegularity {V : Type u} [ModelEPUPIR V] (a : V) : (∃ (b : V), b ∈ a) → ∃ (b : V), b ∈ a ∧ ∀ (c : V), c ∈ a → c ∉ b

The Regularity axiom described externally.

theorem FirstOrder.ZFC.no_loop {V : Type u} [ModelEPUPIR V] (a : V) : a ∉ a

No set satisfies a∈a.

theorem FirstOrder.ZFC.int_no_loop {V : Type u} [ModelEPUPIR V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : (ϕnotElt (bv'' n) (bv'' n)).all.Realize s xs

No set satisfies a∈a internally.

def FirstOrder.ZFC.intIsSeparation {n : ℕ} (ϕ : Language.LZFC.BoundedFormula ℕ n) : Language.LZFC.BoundedFormula ℕ n

t = {x∈(bv n) : ϕ}.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.ZFC.intIsSeparation' {n : ℕ} (ϕ : Language.LZFC.BoundedFormula ℕ n) (n' : ℕ) (t₁ t₂ : Language.LZFC.Term (ℕ ⊕ Fin (n + n'))) : Language.LZFC.BoundedFormula ℕ (n + n')

Generalized separation formula: t₂ = {x ∈ t₁ : ϕ} lifted by n'.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.ZFC.ExtIsSeparation {V : Type u} [ModelSets V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (ϕ : Language.LZFC.BoundedFormula ℕ n) (a b : V) : Prop

Externally, b = {x ∈ a : ϕ}.

Equations

• FirstOrder.ZFC.ExtIsSeparation s xs ϕ a b = ∀ (x : V), x ∈ b ↔ x ∈ a ∧ ϕ.Realize (FirstOrder.Language.BoundedFormula.replaceInitialValues s ![x]) xs

@[simp]

theorem FirstOrder.ZFC.realize_separation {V : Type u} [ModelSets V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (ϕ : Language.LZFC.BoundedFormula ℕ n) : (intIsSeparation ϕ).Realize s xs ↔ ExtIsSeparation s xs ϕ (s 0) (s 1)

@[simp]

theorem FirstOrder.ZFC.realize_separation'_no_lift {V : Type u} [ModelSets V] {n : ℕ} (ϕ : Language.LZFC.BoundedFormula ℕ n) (t₁ t₂ : Language.LZFC.Term (ℕ ⊕ Fin n)) (s : ℕ → V) (xs : Fin n → V) : (intIsSeparation' ϕ 0 t₁ t₂).Realize s xs ↔ ExtIsSeparation s xs ϕ (Language.Term.realize (Sum.elim s xs) t₁) (Language.Term.realize (Sum.elim s xs) t₂)

@[simp]

theorem FirstOrder.ZFC.realize_separation'_lift {V : Type u} [ModelSets V] {n : ℕ} (ϕ : Language.LZFC.BoundedFormula ℕ n) (n' : ℕ) (h_n' : n' > 0) (t₁ t₂ : Language.LZFC.Term (ℕ ⊕ Fin (n + n'))) (s : ℕ → V) (xs : Fin (n + n') → V) : (intIsSeparation' ϕ n' t₁ t₂).Realize s xs ↔ ExtIsSeparation s xs (Language.BoundedFormula.liftAt n' n ϕ) (Language.Term.realize (Sum.elim s xs) t₁) (Language.Term.realize (Sum.elim s xs) t₂)

theorem FirstOrder.ZFC.lift_ExtIsSeparation {V : Type u} [ModelSets V] {n n' : ℕ} {h_n' : n' > 0} {s : ℕ → V} {xs : Fin (n + n') → V} {ϕ : Language.LZFC.BoundedFormula ℕ n} {a b : V} : ExtIsSeparation s xs (Language.BoundedFormula.liftAt n' n ϕ) a b ↔ ExtIsSeparation s (fun (k : Fin n) => xs (Fin.castAdd n' k)) ϕ a b

A lifted ExtIsSeparation is equivalent to the unlifted one with restricted context.

class FirstOrder.ZFC.ModelComprehension (V : Type u) extends FirstOrder.ZFC.ModelSets V : Type u

Model with the Comprehension schema.

• funMap {n : ℕ} : LZFC.Functions n → (Fin n → V) → V
• RelMap {n : ℕ} : LZFC.Relations n → (Fin n → V) → Prop
• default : V
• isEltOf : V → V → Prop
• interpret_is_elt_of {a b : V} : a ∈ b ↔ Language.Structure.RelMap isEltOfTwo ![a, b]
• extensionality {a b : V} : (∀ (z : V), z ∈ a ↔ z ∈ b) → a = b
• comprehension_schema {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (ϕ : Language.LZFC.BoundedFormula ℕ n) : (intIsSeparation' ϕ 2 (bv'' n) (bv'' (n + 1))).ex.all.Realize s xs

  The model satisfies the comprehension schema.

theorem FirstOrder.ZFC.ext_comprehension {V : Type u} [ModelComprehension V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (ϕ : Language.LZFC.BoundedFormula ℕ n) (a : V) : ∃ (b : V), ExtIsSeparation s xs ϕ a b

The Comprehension schema described externally.

class FirstOrder.ZFC.ModelEPUPIC (V : Type u) extends FirstOrder.ZFC.ModelEPUPI V, FirstOrder.ZFC.ModelComprehension V : Type u

Model with emptyset, pairing, union, powerset, infinity, and comprehension.

• funMap {n : ℕ} : LZFC.Functions n → (Fin n → V) → V
• RelMap {n : ℕ} : LZFC.Relations n → (Fin n → V) → Prop
• default : V
• isEltOf : V → V → Prop
• interpret_is_elt_of {a b : V} : a ∈ b ↔ Language.Structure.RelMap isEltOfTwo ![a, b]
• extensionality {a b : V} : (∀ (z : V), z ∈ a ↔ z ∈ b) → a = b
• emptyset_exists {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : (intIsEmptyset' (bv' 0)).ex.Realize s xs
• pairing (s : ℕ → V) (xs : Fin 0 → V) : (intIsPair.liftAndReplaceFV 3 0 ![bv 3 0, bv 3 1, bv 3 2]).ex.all.all.Realize s xs
• union_exists (s : ℕ → V) (xs : Fin 0 → V) : (intIsUnion.liftAndReplaceFV 2 0 ![bv' 0, bv' 1]).ex.all.Realize s xs
• powerset_exists (s : ℕ → V) (xs : Fin 0 → V) : (intIsPowerset.liftAndReplaceFV 2 0 ![bv 2 0, bv 2 1]).ex.all.Realize s xs
• infinity_exists {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : (intIsInductive' (bv'' n)).ex.Realize s xs
• comprehension_schema {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (ϕ : Language.LZFC.BoundedFormula ℕ n) : (intIsSeparation' ϕ 2 (bv'' n) (bv'' (n + 1))).ex.all.Realize s xs

def FirstOrder.ZFC.intIsOmega {n : ℕ} : Language.LZFC.BoundedFormula ℕ n

Make a formula for fv 0 is ω.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.ZFC.intIsOmega' {n : ℕ} (t : Language.LZFC.Term (ℕ ⊕ Fin n)) : Language.LZFC.BoundedFormula ℕ n

Make a formula for t is ω.

Equations

• FirstOrder.ZFC.intIsOmega' t = FirstOrder.ZFC.intIsOmega.replaceFV (FirstOrder.Language.BoundedFormula.makeTsN ![t])

def FirstOrder.ZFC.ExtIsOmega {V : Type u} [ModelEPUPI V] (a : V) : Prop

Describe a is ω.

Equations

• FirstOrder.ZFC.ExtIsOmega a = (FirstOrder.ZFC.ExtIsInductive a ∧ ∀ (b : V), FirstOrder.ZFC.ExtIsInductive b → a ⊆ b)

@[simp]

theorem FirstOrder.ZFC.realize_is_omega {V : Type u} [ModelEPUPI V] {n : ℕ} {s : ℕ → V} {xs : Fin n → V} : intIsOmega.Realize s xs ↔ ExtIsOmega (s 0)

@[simp]

theorem FirstOrder.ZFC.realize_is_omega' {V : Type u} [ModelEPUPI V] {n : ℕ} {s : ℕ → V} {xs : Fin n → V} (t : Language.LZFC.Term (ℕ ⊕ Fin n)) : (intIsOmega' t).Realize s xs ↔ ExtIsOmega (Language.Term.realize (Sum.elim s xs) t)

theorem FirstOrder.ZFC.ext_omega_exists {V : Type u} [ModelEPUPIC V] {n : ℕ} {s : ℕ → V} {xs : Fin n → V} : ∃ (omega : V), ExtIsOmega omega

ω exists.

theorem FirstOrder.ZFC.ext_omega_minus_emptyset {V : Type u} [ModelEPUPIC V] (emp : V) : ExtIsEmptyset emp → ∀ (omega : V), ExtIsOmega omega → ∃ (b : V), ∀ (x : V), x ∈ b ↔ x ∈ omega ∧ x ≠ emp

ω minus the emptyset exists as a separation.

theorem FirstOrder.ZFC.int_omega_minus_emptyset {V : Type u} [ModelEPUPIC V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) : ((intIsEmptyset' (bv'' n)).imp ((intIsOmega' (bv'' (n + 1))).imp ((ϕelt (bv'' (n + 3)) (bv'' (n + 2))).iff (ϕelt (bv'' (n + 3)) (bv'' (n + 1))∧'intNotEqual (bv'' (n + 3)) (bv'' n))).all.ex)).all.all.Realize s xs

ω minus the emptyset internally.

theorem FirstOrder.ZFC.omega_closed_under_succ {V : Type u} [ModelEPUPIC V] (omega : V) : ExtIsOmega omega → ∀ (x y : V), x ∈ omega → ExtIsSuccessor x y → y ∈ omega

ω is closed under the successor operation.

theorem FirstOrder.ZFC.ext_induction {V : Type u} [ModelEPUPIC V] {n : ℕ} {s : ℕ → V} {xs : Fin n → V} (ϕ : Language.LZFC.BoundedFormula ℕ n) (emp : V) : ExtIsEmptyset emp → ∀ (omega : V), ExtIsOmega omega → ϕ.Realize (Language.BoundedFormula.replaceInitialValues s ![emp]) xs → (∀ (x : V), ϕ.Realize (Language.BoundedFormula.replaceInitialValues s ![x]) xs → ∀ (y : V), ExtIsSuccessor x y → ϕ.Realize (Language.BoundedFormula.replaceInitialValues s ![y]) xs) → ∀ (x : V), x ∈ omega → ϕ.Realize (Language.BoundedFormula.replaceInitialValues s ![x]) xs

The principle of mathematical induction for ω.

theorem FirstOrder.ZFC.int_induction {V : Type u} [ModelEPUPIC V] {n : ℕ} {s : ℕ → V} {xs : Fin n → V} (ϕ : Language.LZFC.BoundedFormula ℕ n) : ((intIsEmptyset' (bv'' n)).imp ((intIsOmega' (bv'' (n + 1))).imp ((ϕ.liftAndReplaceFV 2 n ![bv'' n]).imp (((ϕ.liftAndReplaceFV 3 n ![bv'' (n + 2)]).imp ((intIsSuccessor' (bv'' (n + 2)) (bv'' (n + 3))).imp (ϕ.liftAndReplaceFV 4 n ![bv'' (n + 3)])).all).all.imp ((ϕelt (bv'' (n + 2)) (bv'' (n + 1))).imp (ϕ.liftAndReplaceFV 3 n ![bv'' (n + 2)])).all))).all).all.Realize s xs

The principle of mathematical induction for ω internally.