Ersatzaxiom

theorem FFL.FirstOrder.SetTheory.replacement_exists_eval {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (φ : SetTheorySemiformula V 2) (X : V) (h : ∀ (x : V), ∃! y : V, (Semiformula.Eval ![x, y] id) φ) : ∃ (Y : V), ∀ (y : V), y ∈ Y ↔ ∃ x ∈ X, (Semiformula.Eval ![x, y] id) φ

theorem FFL.FirstOrder.SetTheory.replacement_rel_exists {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (X : V) (R : V → V → Prop) (h : ∀ (x : V), ∃! y : V, R x y) (hR : ℒₛₑₜ-relation R) : ∃ (Y : V), ∀ (y : V), y ∈ Y ↔ ∃ x ∈ X, R x y

Replacement exists (for a relation).

theorem FFL.FirstOrder.SetTheory.replacement_rel_existsUnique {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (X : V) (R : V → V → Prop) (h : ∀ (x : V), ∃! y : V, R x y) (hR : ℒₛₑₜ-relation R) : ∃! Y : V, ∀ (y : V), y ∈ Y ↔ ∃ x ∈ X, R x y

Replacement exists uniquely (for a relation).

theorem FFL.FirstOrder.SetTheory.replacement_existsUnique {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (X : V) (F : V → V) (hF : ℒₛₑₜ-function₁ F) : ∃! Y : V, ∀ (y : V), y ∈ Y ↔ ∃ x ∈ X, y = F x

Replacement exists uniquely for a function.

theorem FFL.FirstOrder.SetTheory.replacement_exists {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (X : V) (F : V → V) (hF : ℒₛₑₜ-function₁ F) : ∃ (Y : V), ∀ (y : V), y ∈ Y ↔ ∃ x ∈ X, y = F x

Replacement exists for a function.

noncomputable def FFL.FirstOrder.SetTheory.replRel {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (R : V → V → Prop) (h : ∀ (x : V), ∃! y : V, R x y) (hR : ℒₛₑₜ-relation R := by definability) (X : V) : V

The axiom of replacement for a relation.

Equations

• FFL.FirstOrder.SetTheory.replRel R h hR X = Classical.choose! ⋯

noncomputable def FFL.FirstOrder.SetTheory.repl {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (F : V → V) (hF : ℒₛₑₜ-function₁ F := by definability) (X : V) : V

The axiom of replacement.

Equations

• FFL.FirstOrder.SetTheory.repl F hF X = Classical.choose! ⋯

Variants of replacement

theorem FFL.FirstOrder.SetTheory.replacement_rel_existsUnique_of_mem_existsUnique {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (X : V) (R : V → V → Prop) (h : ∀ x ∈ X, ∃! y : V, R x y) (hR : ℒₛₑₜ-relation R) : ∃! Y : V, ∀ (y : V), y ∈ Y ↔ ∃ x ∈ X, R x y

A stronger variant of (unique existence of) replacement, which only requires uniqueness on X. The statement of this lemma is thanks to tosiaki.

theorem FFL.FirstOrder.SetTheory.replacement_rel_exists_of_mem_existsUnique {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (X : V) (R : V → V → Prop) (h : ∀ x ∈ X, ∃! y : V, R x y) (hR : ℒₛₑₜ-relation R) : ∃ (Y : V), ∀ (y : V), y ∈ Y ↔ ∃ x ∈ X, R x y

A stronger variant of replacement, which only requires uniqueness on X. The statement of this lemma is thanks to tosiaki.

noncomputable def FFL.FirstOrder.SetTheory.replRelOverSet {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (X : V) (R : V → V → Prop) (h : ∀ x ∈ X, ∃! y : V, R x y) (hR : ℒₛₑₜ-relation R := by definability) : V

The axiom of replacement, only assuming uniqueness on X.

Equations

• FFL.FirstOrder.SetTheory.replRelOverSet X R h hR = Classical.choose! ⋯

Various lemmas

@[simp]

theorem FFL.FirstOrder.SetTheory.replRel_spec {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] {X y : V} {R : V → V → Prop} {h : ∀ x ∈ X, ∃! y : V, R x y} (hR : ℒₛₑₜ-relation R) : y ∈ replRelOverSet X R h hR ↔ ∃ x ∈ X, R x y

@[simp]

theorem FFL.FirstOrder.SetTheory.repl_spec {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] {X y : V} {F : V → V} (hF : ℒₛₑₜ-function₁ F) : y ∈ repl F hF X ↔ ∃ x ∈ X, y = F x

@[simp]

theorem FFL.FirstOrder.SetTheory.replRelOverSet_spec {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] {X y : V} {R : V → V → Prop} {h : ∀ x ∈ X, ∃! y : V, R x y} (hR : ℒₛₑₜ-relation R) : y ∈ replRelOverSet X R h hR ↔ ∃ x ∈ X, R x y

@[simp]

instance FFL.FirstOrder.SetTheory.repl_definable {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] {F : V → V} [hF : ℒₛₑₜ-function₁ F] : ℒₛₑₜ-function₁ repl F hF

Definability Gadgets for Replacement

structure FFL.FirstOrder.SetTheory.Repl.Blueprint (arity : ℕ) : Type

• graph : SetTheorySemisentence (arity + 2)

def FFL.FirstOrder.SetTheory.Repl.Blueprint.resultDef {arity : ℕ} (b : Blueprint arity) : SetTheorySemisentence (arity + 2)

Equations

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

structure FFL.FirstOrder.SetTheory.Repl.Construction (V : Type u_1) [SetStructure V] {arity : ℕ} (b : Blueprint arity) : Type u_1

• map : (Fin arity → V) → V → V
• map_defined : DefinedFunction (fun (v : Fin (arity + 1) → V) => self.map (fun (x : Fin arity) => v x.succ) (v 0)) b.graph

instance FFL.FirstOrder.SetTheory.Repl.Construction.map_definable {V : Type u_1} [SetStructure V] {arity : ℕ} {b : Blueprint arity} (c : Construction V b) : ℒₛₑₜ.DefinableFunction fun (v : Fin (arity + 1) → V) => c.map (fun (x : Fin arity) => v x.succ) (v 0)

noncomputable def FFL.FirstOrder.SetTheory.Repl.Construction.result {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] {arity : ℕ} {b : Blueprint arity} (c : Construction V b) (v : Fin arity → V) : V → V

Equations

• c.result v = FFL.FirstOrder.SetTheory.repl (c.map v) ⋯

theorem FFL.FirstOrder.SetTheory.Repl.Construction.result_defined {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] {arity : ℕ} {b : Blueprint arity} (c : Construction V b) : DefinedFunction (fun (v : Fin (arity + 1) → V) => c.result (fun (x : Fin arity) => v x.succ) (v 0)) b.resultDef

@[simp]

theorem FFL.FirstOrder.SetTheory.Repl.Construction.eval_resultDef {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] {arity : ℕ} {b : Blueprint arity} (c : Construction V b) {v : Fin (arity + 2) → V} : (Semiformula.Evalb v) b.resultDef ↔ v 0 = c.result (fun (x : Fin arity) => v x.succ.succ) (v 1)

@[simp]

theorem FFL.FirstOrder.SetTheory.Repl.Construction.mem_result {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] {arity : ℕ} {b : Blueprint arity} (c : Construction V b) {v : Fin arity → V} {y X : V} : y ∈ c.result v X ↔ ∃ x ∈ X, y = c.map v x