The Replacement Axiom

Main Definitions

• A FirstOrder.ZFC.RelByFormula defines the relation defined by a formula.
• A FirstOrder.ZFC.intIsFunctFormula defines a formula for ϕ describes a function. A FirstOrder.ZFC.EntIsFunctFormula defines ϕ describes a function externally.
• A FirstOrder.ZFC.intIsImage defines the formula for fv 1 is the image of the function defined by ϕ of fv 0.
• A FirstOrder.ZFC.ModelReplacement is a class of models of Set Theory with the replacement schema.
• A FirstOrder.ZFC.ModelZF is a class of models of ZF.

Main Statements

• Various "realize" theorems are proved.

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

Make a formula for ϕ describes a function.

Equations

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

def FirstOrder.ZFC.RelByFormula {V : Type u} [ModelSets V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (ϕ : Language.LZFC.BoundedFormula ℕ n) {k : ℕ} (xs1 : Fin (k + 1) → V) : Prop

Find the (k+1)-ary relation defined by a formula.

Equations

• FirstOrder.ZFC.RelByFormula s xs ϕ xs1 = ϕ.Realize (FirstOrder.Language.BoundedFormula.replaceInitialValues s xs1) xs

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

Dexcribe ϕ describes a function.

Equations

• FirstOrder.ZFC.ExtIsFunctFormula s xs ϕ = ∀ (x y₁ y₂ : V), FirstOrder.ZFC.RelByFormula s xs ϕ ![x, y₁] → FirstOrder.ZFC.RelByFormula s xs ϕ ![x, y₂] → y₁ = y₂

theorem FirstOrder.ZFC.realize_is_funct_formula {V : Type u} [ModelSets V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (ϕ : Language.LZFC.BoundedFormula ℕ n) : (intIsFunctFormula ϕ).Realize s xs ↔ ExtIsFunctFormula s xs ϕ

The realization of intIsFunctFormula ϕ matches ExtIsFunctFormula ϕ.

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

Make a formula for fv 1 is the image of fv 0 under the relation defined by ϕ.

Equations

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

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

Describe b is the image of a under the relation defined by ϕ.

Equations

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

@[simp]

theorem FirstOrder.ZFC.replaceInitialValues_replaceInitialValues {V : Type u} {n m : ℕ} {h : n ≤ m} {s : ℕ → V} {xs1 : Fin (n + 1) → V} {xs2 : Fin (m + 1) → V} : Language.BoundedFormula.replaceInitialValues (Language.BoundedFormula.replaceInitialValues s xs1) xs2 = Language.BoundedFormula.replaceInitialValues s xs2

replaceInitialValues composed with a larger replacement collapses.

@[simp]

theorem FirstOrder.ZFC.realize_is_image {V : Type u} [ModelSets V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (ϕ : Language.LZFC.BoundedFormula ℕ n) (a b : V) : (intIsImage ϕ).Realize (Language.BoundedFormula.replaceInitialValues s ![a, b]) xs ↔ ExtIsImage s xs ϕ a b

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

Model with the Replacement 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
• replacement_schema {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (ϕ : Language.LZFC.BoundedFormula ℕ n) : ((intIsFunctFormula ϕ).imp ((Language.BoundedFormula.liftAt 2 n (intIsImage ϕ)).replaceFV (Language.BoundedFormula.makeTsN ![bv'' n, bv'' (n + 1)])).ex.all).Realize s xs

  The model satisfies the replacement schema.

theorem FirstOrder.ZFC.ext_replacement {V : Type u} [ModelReplacement V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (ϕ : Language.LZFC.BoundedFormula ℕ n) : ExtIsFunctFormula s xs ϕ → ∀ (a : V), ∃ (b : V), ExtIsImage s xs ϕ a b

The Replacement described externally.

class FirstOrder.ZFC.ModelPR (V : Type u) extends FirstOrder.ZFC.ModelPairing V, FirstOrder.ZFC.ModelReplacement V : Type u

Model with pairing and replacement.

• 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
• replacement_schema {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (ϕ : Language.LZFC.BoundedFormula ℕ n) : ((intIsFunctFormula ϕ).imp ((Language.BoundedFormula.liftAt 2 n (intIsImage ϕ)).replaceFV (Language.BoundedFormula.makeTsN ![bv'' n, bv'' (n + 1)])).ex.all).Realize s xs

theorem FirstOrder.ZFC.ext_test {V : Type u} [ModelPR V] (s : ℕ → V) (xs : Fin 0 → V) (a : V) : ∃ (b : V), ExtIsImage s xs intIsSingleton a b

The image of intIsSingleton exists as a witness to replacement.

theorem FirstOrder.ZFC.int_test {V : Type u} [ModelPR V] (s : ℕ → V) (xs : Fin 0 → V) : ((intIsImage intIsSingleton).liftAndReplaceFV 2 0 ![bv'' 0, bv'' 1]).ex.all.Realize s xs

The image of intIsSingleton exists as a witness to replacement, internally.

class FirstOrder.ZFC.ModelZF (V : Type u) extends FirstOrder.ZFC.ModelEmptyset V, FirstOrder.ZFC.ModelPairing V, FirstOrder.ZFC.ModelUnion V, FirstOrder.ZFC.ModelPowerset V, FirstOrder.ZFC.ModelInfinity V, FirstOrder.ZFC.ModelRegularity V, FirstOrder.ZFC.ModelComprehension V, FirstOrder.ZFC.ModelReplacement V : Type u

Model of ZF: all the standard axioms together.

• 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
• 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
• replacement_schema {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (ϕ : Language.LZFC.BoundedFormula ℕ n) : ((intIsFunctFormula ϕ).imp ((Language.BoundedFormula.liftAt 2 n (intIsImage ϕ)).replaceFV (Language.BoundedFormula.makeTsN ![bv'' n, bv'' (n + 1)])).ex.all).Realize s xs