Documentation

Arithmetization.ISigmaOne.HFS.PRF

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

Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        structure LO.Arith.PR.Construction (V : Type u_1) [LO.ORingStruc V] {k : β„•} (p : LO.Arith.PR.Blueprint k) :
        Type u_1
        Instances For
          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
          Equations
          Instances For
            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
            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
            Equations
            Instances For
              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
              • β‹― = β‹―