Documentation

Foundation.FirstOrder.Arithmetic.R0.Representation

source
theorem FFL.FirstOrder.Arithmetic.term_primrec {ξ : Type u_1} {k : ℕ} {f : ξ → ℕ} (t : ArithmeticSemiterm ξ k) :
Primrec fun (v : List.Vector ℕ k) => Semiterm.val v.get f t
source
theorem FFL.FirstOrder.Arithmetic.primrecPred_ball {ξ : Type u_1} (ε : ξ → ℕ) {n : ℕ} (t : ArithmeticSemiterm ξ n) {ψ : ArithmeticSemiformula ξ (n + 1)} (h : PrimrecPred fun (v : List.Vector ℕ (n + 1)) => (Semiformula.Eval v.get ε) ψ) :
PrimrecPred fun (v : List.Vector ℕ n) => ∀ x < Semiterm.val v.get ε t, (Semiformula.Eval (x :> v.get) ε) ψ
source
theorem FFL.FirstOrder.Arithmetic.primrecPred_bexs {ξ : Type u_1} (ε : ξ → ℕ) {n : ℕ} (t : ArithmeticSemiterm ξ n) {ψ : ArithmeticSemiformula ξ (n + 1)} (h : PrimrecPred fun (v : List.Vector ℕ (n + 1)) => (Semiformula.Eval v.get ε) ψ) :
PrimrecPred fun (v : List.Vector ℕ n) => ∃ x < Semiterm.val v.get ε t, (Semiformula.Eval (x :> v.get) ε) ψ
source
theorem FFL.FirstOrder.Arithmetic.delta0_primrec {ξ : Type u_1} (ε : ξ → ℕ) {k : ℕ} {φ : ArithmeticSemiformula ξ k} (hp : Hierarchy 𝚺 0 φ) :
PrimrecPred fun (v : List.Vector ℕ k) => (Semiformula.Eval v.get ε) φ
source
theorem FFL.FirstOrder.Arithmetic.sigma1_re {ξ : Type u_1} (ε : ξ → ℕ) {k : ℕ} {φ : ArithmeticSemiformula ξ k} (hp : Hierarchy 𝚺 1 φ) :
REPred fun (v : List.Vector ℕ k) => (Semiformula.Eval v.get ε) φ
source
def FFL.FirstOrder.Arithmetic.codeAux {k : ℕ} :
Nat.ArithPart₁.Code k → ArithmeticFormula (Fin (k + 1))
Equations
Instances For
    source
    def FFL.FirstOrder.Arithmetic.code {k : ℕ} (c : Nat.ArithPart₁.Code k) :
    ArithmeticSemisentence (k + 1)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem FFL.FirstOrder.Arithmetic.code_sigma_one {k : ℕ} (c : Nat.ArithPart₁.Code k) :
      Hierarchy 𝚺 1 (code c)
      source
      @[simp]
      theorem FFL.FirstOrder.Arithmetic.natCast_nat' (n : ℕ) :
      ↑n = n
      source
      theorem FFL.FirstOrder.Arithmetic.models_code {k : ℕ} {c : Nat.ArithPart₁.Code k} {f : List.Vector ℕ k →. ℕ} (hc : c.eval f) (y : ℕ) (v : Fin k → ℕ) :
      (Semiformula.Evalb (y :> v)) (code c) ↔ y ∈ f (List.Vector.ofFn v)
      source
      noncomputable def FFL.FirstOrder.Arithmetic.codeOfPartrec' {k : ℕ} (f : List.Vector ℕ k →. ℕ) :
      ArithmeticSemisentence (k + 1)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem FFL.FirstOrder.Arithmetic.codeOfPartrec'_spec {k : ℕ} {f : List.Vector ℕ k →. ℕ} (hf : Nat.Partrec' f) {y : ℕ} {v : Fin k → ℕ} :
        (Semiformula.Evalb (y :> v)) (codeOfPartrec' f) ↔ y ∈ f (List.Vector.ofFn v)
        source
        theorem FFL.FirstOrder.Arithmetic.code_uniq {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {k : ℕ} {c : Nat.ArithPart₁.Code k} {v : Fin k → M} {z z' : M} :
        (Semiformula.Evalb (z :> v)) (code c) → (Semiformula.Evalb (z' :> v)) (code c) → z = z'
        source
        noncomputable def FFL.FirstOrder.Arithmetic.codeOfREPred (p : ℕ → Prop) :
        ArithmeticSemisentence 1
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem FFL.FirstOrder.Arithmetic.codeOfREPred_spec {p : ℕ → Prop} (hp : REPred p) {x : ℕ} :
          (Semiformula.Evalb ![x]) (codeOfREPred p) ↔ p x
          source
          theorem FFL.FirstOrder.Arithmetic.rePred_weak_representation {T : ArithmeticTheory} [𝗥₀ ⪯ T] [T.SoundOnHierarchy 𝚺 1] {p : ℕ → Prop} (hp : REPred p) {x : ℕ} :
          p x ↔ T ⊢ (codeOfREPred p)/[↑x]

          Weak representation of a r.e. predicate

          source
          noncomputable def FFL.FirstOrder.Arithmetic.codeOfComputablePred (p : ℕ → Prop) :
          ArithmeticSemisentence 1
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem FFL.FirstOrder.Arithmetic.codeOfComputablePred_sigma1 (p : ℕ → Prop) :
            Hierarchy 𝚺 1 (codeOfComputablePred p)
            source
            theorem FFL.FirstOrder.Arithmetic.codeOfComputablePred_provable {p : ℕ → Prop} {T : ArithmeticTheory} {x : ℕ} [𝗥₀ ⪯ T] (hp : ComputablePred p) (h : p x) :
            T ⊢ (codeOfComputablePred p)/[↑x]

            Positive representation of a computable predicate.

            source
            theorem FFL.FirstOrder.Arithmetic.codeOfComputablePred_provable_neg {p : ℕ → Prop} {T : ArithmeticTheory} {x : ℕ} [𝗣𝗔⁻ ⪯ T] (hp : ComputablePred p) (h : ¬p x) :
            T ⊢ ∼(codeOfComputablePred p)/[↑x]

            Negative representation of a computable predicate.

            source
            theorem FFL.FirstOrder.Arithmetic.rePred_iff_sigma1 {p : ℕ → Prop} :
            REPred p ↔ 𝚺₁-Predicate p
            source
            theorem FFL.FirstOrder.Arithmetic.computablePred_iff_delta1 {p : ℕ → Prop} :
            ComputablePred p ↔ 𝚫₁-Predicate p
            source
            theorem FFL.FirstOrder.Arithmetic.computable_iff_sigma1 {f : ℕ → ℕ} :
            Computable f ↔ 𝚺₁-Function₁ f
            source
            theorem FFL.FirstOrder.Arithmetic.computable₂_iff_sigma1 {f : ℕ → ℕ → ℕ} :
            Computable₂ f ↔ 𝚺₁-Function₂ f