Fixpoint Construction

structure LO.Arith.Fixpoint.Blueprint (k : ℕ) : Type

• core : 𝚫₁.Semisentence (k + 2)

instance LO.Arith.Fixpoint.Blueprint.instCoeSemisentenceDeltaOneHAddNatOfNat {k : ℕ} : Coe (LO.Arith.Fixpoint.Blueprint k) (𝚫₁.Semisentence (k + 2))

Equations

• LO.Arith.Fixpoint.Blueprint.instCoeSemisentenceDeltaOneHAddNatOfNat = { coe := LO.Arith.Fixpoint.Blueprint.core }

def LO.Arith.Fixpoint.Blueprint.succDef {k : ℕ} (φ : LO.Arith.Fixpoint.Blueprint k) : 𝚺₁.Semisentence (k + 3)

Equations

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

def LO.Arith.Fixpoint.Blueprint.prBlueprint {k : ℕ} (φ : LO.Arith.Fixpoint.Blueprint k) : LO.Arith.PR.Blueprint k

Equations

• φ.prBlueprint = { zero := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma (“!!(LO.FirstOrder.Semiterm.bvar 0) = 0”) ⋯, succ := φ.succDef }

def LO.Arith.Fixpoint.Blueprint.limSeqDef {k : ℕ} (φ : LO.Arith.Fixpoint.Blueprint k) : 𝚺₁.Semisentence (k + 2)

Equations

• φ.limSeqDef = φ.prBlueprint.resultDef

def LO.Arith.Fixpoint.Blueprint.fixpointDef {k : ℕ} (φ : LO.Arith.Fixpoint.Blueprint k) : 𝚺₁.Semisentence (k + 1)

Equations

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

def LO.Arith.Fixpoint.Blueprint.fixpointDefΔ₁ {k : ℕ} (φ : LO.Arith.Fixpoint.Blueprint k) : 𝚫₁.Semisentence (k + 1)

Equations

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

structure LO.Arith.Fixpoint.Construction (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} (φ : LO.Arith.Fixpoint.Blueprint k) : Type u_1

• Φ : (Fin k → V) → Set V → V → Prop
• defined : LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin k.succ.succ → V) => self.Φ (fun (x : Fin k) => v x.succ.succ) {x : V | x ∈ v 1} (v 0)) φ.core
• monotone : ∀ {C C' : Set V}, C ⊆ C' → ∀ {v : Fin k → V} {x : V}, self.Φ v C x → self.Φ v C' x

theorem LO.Arith.Fixpoint.Construction.defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (self : LO.Arith.Fixpoint.Construction V φ) : LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin k.succ.succ → V) => self.Φ (fun (x : Fin k) => v x.succ.succ) {x : V | x ∈ v 1} (v 0)) φ.core

theorem LO.Arith.Fixpoint.Construction.monotone {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (self : LO.Arith.Fixpoint.Construction V φ) {C : Set V} {C' : Set V} (h : C ⊆ C') {v : Fin k → V} {x : V} : self.Φ v C x → self.Φ v C' x

class LO.Arith.Fixpoint.Construction.Finite (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) : Type

• finite : ∀ {C : Set V} {v : Fin k → V} {x : V}, c.Φ v C x → ∃ (m : V), c.Φ v {y : V | y ∈ C ∧ y < m} x

theorem LO.Arith.Fixpoint.Construction.Finite.finite {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} {c : LO.Arith.Fixpoint.Construction V φ} [self : LO.Arith.Fixpoint.Construction.Finite V c] {C : Set V} {v : Fin k → V} {x : V} : c.Φ v C x → ∃ (m : V), c.Φ v {y : V | y ∈ C ∧ y < m} x

class LO.Arith.Fixpoint.Construction.StrongFinite (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) : Type

• strong_finite : ∀ {C : Set V} {v : Fin k → V} {x : V}, c.Φ v C x → c.Φ v {y : V | y ∈ C ∧ y < x} x

theorem LO.Arith.Fixpoint.Construction.StrongFinite.strong_finite {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} {c : LO.Arith.Fixpoint.Construction V φ} [self : LO.Arith.Fixpoint.Construction.StrongFinite V c] {C : Set V} {v : Fin k → V} {x : V} : c.Φ v C x → c.Φ v {y : V | y ∈ C ∧ y < x} x

instance LO.Arith.Fixpoint.instFiniteOfStrongFinite (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) [LO.Arith.Fixpoint.Construction.StrongFinite V c] : LO.Arith.Fixpoint.Construction.Finite V c

Equations

• LO.Arith.Fixpoint.instFiniteOfStrongFinite V c = { finite := ⋯ }

theorem LO.Arith.Fixpoint.Construction.eval_formula {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) (v : Fin k.succ.succ → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val φ.core) ↔ c.Φ (fun (x : Fin k) => v x.succ.succ) {x : V | x ∈ v 1} (v 0)

theorem LO.Arith.Fixpoint.Construction.succ_existsUnique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) (v : Fin k → V) (s : V) (ih : V) : ∃! u : V, ∀ (x : V), x ∈ u ↔ x ≤ s ∧ c.Φ v {z : V | z ∈ ih} x

def LO.Arith.Fixpoint.Construction.succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) (v : Fin k → V) (s : V) (ih : V) : V

Equations

• c.succ v s ih = Classical.choose! ⋯

theorem LO.Arith.Fixpoint.Construction.mem_succ_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {x : V} {v : Fin k → V} {s : V} {ih : V} : x ∈ c.succ v s ih ↔ x ≤ s ∧ c.Φ v {z : V | z ∈ ih} x

theorem LO.Arith.Fixpoint.Construction.succ_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin (k + 2) → V) => c.succ (fun (x : Fin k) => v x.succ.succ) (v 1) (v 0)) φ.succDef

theorem LO.Arith.Fixpoint.Construction.eval_succDef {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) (v : Fin (k + 3) → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val φ.succDef) ↔ v 0 = c.succ (fun (x : Fin k) => v x.succ.succ.succ) (v 2) (v 1)

def LO.Arith.Fixpoint.Construction.prConstruction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) : LO.Arith.PR.Construction V φ.prBlueprint

Equations

• c.prConstruction = { zero := fun (x : Fin k → V) => ∅, succ := c.succ, zero_defined := ⋯, succ_defined := ⋯ }

def LO.Arith.Fixpoint.Construction.limSeq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) (v : Fin k → V) (s : V) : V

Equations

• c.limSeq v s = c.prConstruction.result v s

@[simp]

theorem LO.Arith.Fixpoint.Construction.limSeq_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {v : Fin k → V} : c.limSeq v 0 = ∅

theorem LO.Arith.Fixpoint.Construction.limSeq_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {v : Fin k → V} (s : V) : c.limSeq v (s + 1) = c.succ v s (c.limSeq v s)

theorem LO.Arith.Fixpoint.Construction.termSet_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin k.succ → V) => c.limSeq (fun (x : Fin k) => v x.succ) (v 0)) φ.limSeqDef

@[simp]

theorem LO.Arith.Fixpoint.Construction.eval_limSeqDef {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) (v : Fin (k + 2) → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val φ.limSeqDef) ↔ v 0 = c.limSeq (fun (x : Fin k) => v x.succ.succ) (v 1)

instance LO.Arith.Fixpoint.Construction.limSeq_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) : 𝚺₁.BoldfaceFunction fun (v : Fin k.succ → V) => c.limSeq (fun (x : Fin k) => v x.succ) (v 0)

Equations

• ⋯ = ⋯

@[simp]

instance LO.Arith.Fixpoint.Construction.limSeq_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {m : ℕ} (Γ : LO.SigmaPiDelta) : { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin k.succ → V) => c.limSeq (fun (x : Fin k) => v x.succ) (v 0)

Equations

• ⋯ = ⋯

theorem LO.Arith.Fixpoint.Construction.mem_limSeq_succ_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {v : Fin k → V} {x : V} {s : V} : x ∈ c.limSeq v (s + 1) ↔ x ≤ s ∧ c.Φ v {z : V | z ∈ c.limSeq v s} x

theorem LO.Arith.Fixpoint.Construction.limSeq_cumulative {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {v : Fin k → V} {s : V} {s' : V} : s ≤ s' → c.limSeq v s ⊆ c.limSeq v s'

theorem LO.Arith.Fixpoint.Construction.mem_limSeq_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {v : Fin k → V} [LO.Arith.Fixpoint.Construction.StrongFinite V c] {u : V} {s : V} : u ∈ c.limSeq v s → u ∈ c.limSeq v (u + 1)

def LO.Arith.Fixpoint.Construction.Fixpoint {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) (v : Fin k → V) (x : V) : Prop

Equations

• c.Fixpoint v x = ∃ (s : V), x ∈ c.limSeq v s

theorem LO.Arith.Fixpoint.Construction.fixpoint_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {v : Fin k → V} [LO.Arith.Fixpoint.Construction.StrongFinite V c] {x : V} : c.Fixpoint v x ↔ x ∈ c.limSeq v (x + 1)

theorem LO.Arith.Fixpoint.Construction.fixpoint_iff_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {v : Fin k → V} {x : V} : c.Fixpoint v x ↔ ∃ (u : V), x ∈ c.limSeq v (u + 1)

theorem LO.Arith.Fixpoint.Construction.finite_upperbound {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {v : Fin k → V} (m : V) : ∃ (s : V), ∀ z < m, c.Fixpoint v z → z ∈ c.limSeq v s

theorem LO.Arith.Fixpoint.Construction.case {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {v : Fin k → V} {x : V} [LO.Arith.Fixpoint.Construction.Finite V c] : c.Fixpoint v x ↔ c.Φ v {z : V | c.Fixpoint v z} x

theorem LO.Arith.Fixpoint.Construction.fixpoint_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) : LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin k.succ → V) => c.Fixpoint (fun (x : Fin k) => v x.succ) (v 0)) φ.fixpointDef

@[simp]

theorem LO.Arith.Fixpoint.Construction.eval_fixpointDef {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) (v : Fin (k + 1) → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val φ.fixpointDef) ↔ c.Fixpoint (fun (x : Fin k) => v x.succ) (v 0)

theorem LO.Arith.Fixpoint.Construction.fixpoint_definedΔ₁ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) [LO.Arith.Fixpoint.Construction.StrongFinite V c] : LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin k.succ → V) => c.Fixpoint (fun (x : Fin k) => v x.succ) (v 0)) φ.fixpointDefΔ₁

@[simp]

theorem LO.Arith.Fixpoint.Construction.eval_fixpointDefΔ₁ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) [LO.Arith.Fixpoint.Construction.StrongFinite V c] (v : Fin (k + 1) → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val φ.fixpointDefΔ₁) ↔ c.Fixpoint (fun (x : Fin k) => v x.succ) (v 0)

theorem LO.Arith.Fixpoint.Construction.induction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {v : Fin k → V} {Γ : LO.SigmaPiDelta} [LO.Arith.Fixpoint.Construction.StrongFinite V c] {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (H : ∀ (C : Set V), (∀ x ∈ C, c.Fixpoint v x ∧ P x) → ∀ (x : V), c.Φ v C x → P x) (x : V) : c.Fixpoint v x → P x