Primitive Recursive Functions in $\mathsf{I} \Sigma_1$

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

• zero : 𝚺₁.Semisentence (k + 1)
• succ : 𝚺₁.Semisentence (k + 3)

def LO.Arith.PR.Blueprint.cseqDef {k : ℕ} (p : LO.Arith.PR.Blueprint k) : 𝚺₁.Semisentence (k + 1)

Equations

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

def LO.Arith.PR.Blueprint.resultDef {k : ℕ} (p : LO.Arith.PR.Blueprint k) : 𝚺₁.Semisentence (k + 2)

Equations

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

def LO.Arith.PR.Blueprint.resultDeltaDef {k : ℕ} (p : LO.Arith.PR.Blueprint k) : 𝚫₁.Semisentence (k + 2)

Equations

• p.resultDeltaDef = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.graphDelta p.resultDef

structure LO.Arith.PR.Construction (V : Type u_1) [LO.ORingStruc V] {k : ℕ} (p : LO.Arith.PR.Blueprint k) : Type u_1

• zero : (Fin k → V) → V
• succ : (Fin k → V) → V → V → V
• zero_defined : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction self.zero p.zero
• succ_defined : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin k.succ.succ → V) => self.succ (fun (x : Fin k) => v x.succ.succ) (v 1) (v 0)) p.succ

theorem LO.Arith.PR.Construction.zero_defined {V : Type u_1} [LO.ORingStruc V] {k : ℕ} {p : LO.Arith.PR.Blueprint k} (self : LO.Arith.PR.Construction V p) : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction self.zero p.zero

theorem LO.Arith.PR.Construction.succ_defined {V : Type u_1} [LO.ORingStruc V] {k : ℕ} {p : LO.Arith.PR.Blueprint k} (self : LO.Arith.PR.Construction V p) : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin k.succ.succ → V) => self.succ (fun (x : Fin k) => v x.succ.succ) (v 1) (v 0)) p.succ

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

Equations

• c.CSeq v s = (LO.Arith.Seq s ∧ ⟪0, c.zero v⟫ ∈ s ∧ ∀ i < LO.Arith.lh s - 1, ∀ (z : V), ⟪i, z⟫ ∈ s → ⟪i + 1, c.succ v i z⟫ ∈ s)

theorem LO.Arith.PR.Construction.cseq_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {p : LO.Arith.PR.Blueprint k} (c : LO.Arith.PR.Construction V p) : LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin (k + 1) → V) => c.CSeq (fun (x : Fin k) => v x.succ) (v 0)) p.cseqDef

@[simp]

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

theorem LO.Arith.PR.Construction.CSeq.seq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {p : LO.Arith.PR.Blueprint k} {c : LO.Arith.PR.Construction V p} {v : Fin k → V} {s : V} (h : c.CSeq v s) : LO.Arith.Seq s

theorem LO.Arith.PR.Construction.CSeq.zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {p : LO.Arith.PR.Blueprint k} {c : LO.Arith.PR.Construction V p} {v : Fin k → V} {s : V} (h : c.CSeq v s) : ⟪0, c.zero v⟫ ∈ s

theorem LO.Arith.PR.Construction.CSeq.succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {p : LO.Arith.PR.Blueprint k} {c : LO.Arith.PR.Construction V p} {v : Fin k → V} {s : V} (h : c.CSeq v s) (i : V) : i < LO.Arith.lh s - 1 → ∀ (z : V), ⟪i, z⟫ ∈ s → ⟪i + 1, c.succ v i z⟫ ∈ s

theorem LO.Arith.PR.Construction.CSeq.unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {p : LO.Arith.PR.Blueprint k} {c : LO.Arith.PR.Construction V p} {v : Fin k → V} {s₁ : V} {s₂ : V} (H₁ : c.CSeq v s₁) (H₂ : c.CSeq v s₂) (h₁₂ : LO.Arith.lh s₁ ≤ LO.Arith.lh s₂) {i : V} (hi : i < LO.Arith.lh s₁) {z₁ : V} {z₂ : V} : ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂

theorem LO.Arith.PR.Construction.CSeq.initial {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {p : LO.Arith.PR.Blueprint k} {c : LO.Arith.PR.Construction V p} {v : Fin k → V} : c.CSeq v !⟦c.zero v⟧

theorem LO.Arith.PR.Construction.CSeq.successor {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {p : LO.Arith.PR.Blueprint k} {c : LO.Arith.PR.Construction V p} {v : Fin k → V} {s : V} {l : V} {z : V} (Hs : c.CSeq v s) (hl : l + 1 = LO.Arith.lh s) (hz : ⟪l, z⟫ ∈ s) : c.CSeq v (s ⁀' c.succ v l z)

theorem LO.Arith.PR.Construction.CSeq.exists {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {p : LO.Arith.PR.Blueprint k} (c : LO.Arith.PR.Construction V p) (v : Fin k → V) (l : V) : ∃ (s : V), c.CSeq v s ∧ l + 1 = LO.Arith.lh s

theorem LO.Arith.PR.Construction.cSeq_result_existsUnique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {p : LO.Arith.PR.Blueprint k} (c : LO.Arith.PR.Construction V p) (v : Fin k → V) (l : V) : ∃! z : V, ∃ (s : V), c.CSeq v s ∧ l + 1 = LO.Arith.lh s ∧ ⟪l, z⟫ ∈ s

def LO.Arith.PR.Construction.result {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {p : LO.Arith.PR.Blueprint k} (c : LO.Arith.PR.Construction V p) (v : Fin k → V) (u : V) : V

Equations

• c.result v u = Classical.choose! ⋯

theorem LO.Arith.PR.Construction.result_spec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {p : LO.Arith.PR.Blueprint k} (c : LO.Arith.PR.Construction V p) (v : Fin k → V) (u : V) : ∃ (s : V), c.CSeq v s ∧ u + 1 = LO.Arith.lh s ∧ ⟪u, c.result v u⟫ ∈ s

@[simp]

theorem LO.Arith.PR.Construction.result_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {p : LO.Arith.PR.Blueprint k} (c : LO.Arith.PR.Construction V p) (v : Fin k → V) : c.result v 0 = c.zero v

@[simp]

theorem LO.Arith.PR.Construction.result_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {p : LO.Arith.PR.Blueprint k} (c : LO.Arith.PR.Construction V p) (v : Fin k → V) (u : V) : c.result v (u + 1) = c.succ v u (c.result v u)

theorem LO.Arith.PR.Construction.result_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {p : LO.Arith.PR.Blueprint k} (c : LO.Arith.PR.Construction V p) (v : Fin k → V) (z : V) (u : V) : z = c.result v u ↔ ∃ (s : V), c.CSeq v s ∧ ⟪u, z⟫ ∈ s

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

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

@[simp]

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

instance LO.Arith.PR.Construction.result_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {p : LO.Arith.PR.Blueprint k} (c : LO.Arith.PR.Construction V p) : 𝚺₁.BoldfaceFunction fun (v : Fin (k + 1) → V) => c.result (fun (x : Fin k) => v x.succ) (v 0)

Equations

• ⋯ = ⋯

instance LO.Arith.PR.Construction.result_definable_delta₁ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} {p : LO.Arith.PR.Blueprint k} (c : LO.Arith.PR.Construction V p) : 𝚫₁.BoldfaceFunction fun (v : Fin (k + 1) → V) => c.result (fun (x : Fin k) => v x.succ) (v 0)

Equations

• ⋯ = ⋯