theorem LO.FirstOrder.Arithmetic.term_primrec {ξ : Type u_1} {k : ℕ} {f : ξ → ℕ} (t : ArithmeticSemiterm ξ k) : Primrec fun (v : List.Vector ℕ k) => Semiterm.val v.get f t

theorem LO.FirstOrder.Arithmetic.sigma1_re {ξ : Type u_1} (ε : ξ → ℕ) {k : ℕ} {φ : ArithmeticSemiformula ξ k} (hp : Hierarchy 𝚺 1 φ) : REPred fun (v : List.Vector ℕ k) => (Semiformula.Eval v.get ε) φ

def LO.FirstOrder.Arithmetic.codeAux {k : ℕ} : Nat.ArithPart₁.Code k → ArithmeticFormula (Fin (k + 1))

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Arithmetic.codeAux (Nat.ArithPart₁.Code.zero k) = (“!!(LO.FirstOrder.Semiterm.fvar 0) = 0”)
• LO.FirstOrder.Arithmetic.codeAux (Nat.ArithPart₁.Code.one k) = (“!!(LO.FirstOrder.Semiterm.fvar 0) = 1”)
• LO.FirstOrder.Arithmetic.codeAux (Nat.ArithPart₁.Code.add i j) = (“!!(LO.FirstOrder.Semiterm.fvar 0) = (!!(LO.FirstOrder.Semiterm.fvar i.succ) + !!(LO.FirstOrder.Semiterm.fvar j.succ))”)
• LO.FirstOrder.Arithmetic.codeAux (Nat.ArithPart₁.Code.mul i j) = (“!!(LO.FirstOrder.Semiterm.fvar 0) = (!!(LO.FirstOrder.Semiterm.fvar i.succ) * !!(LO.FirstOrder.Semiterm.fvar j.succ))”)
• LO.FirstOrder.Arithmetic.codeAux (Nat.ArithPart₁.Code.proj i) = (“!!(LO.FirstOrder.Semiterm.fvar 0) = !!(LO.FirstOrder.Semiterm.fvar i.succ)”)

def LO.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.

@[simp]

theorem LO.FirstOrder.Arithmetic.code_sigma_one {k : ℕ} (c : Nat.ArithPart₁.Code k) : Hierarchy 𝚺 1 (code c)

@[simp]

theorem LO.FirstOrder.Arithmetic.natCast_nat' (n : ℕ) : ↑n = n

theorem LO.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)

noncomputable def LO.FirstOrder.Arithmetic.codeOfPartrec' {k : ℕ} (f : List.Vector ℕ k →. ℕ) : ArithmeticSemisentence (k + 1)

Equations

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

theorem LO.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)

noncomputable def LO.FirstOrder.Arithmetic.codeOfREPred (p : ℕ → Prop) : ArithmeticSemisentence 1

Equations

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

theorem LO.FirstOrder.Arithmetic.codeOfREPred_spec {p : ℕ → Prop} (hp : REPred p) {x : ℕ} : (Semiformula.Evalb ![x]) (codeOfREPred p) ↔ p x

theorem LO.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

theorem LO.FirstOrder.Arithmetic.rePred_iff_sigma1 {p : ℕ → Prop} : REPred p ↔ 𝚺₁-Predicate p

theorem LO.FirstOrder.Arithmetic.computablePred_iff_delta1 {p : ℕ → Prop} : ComputablePred p ↔ 𝚫₁-Predicate p

theorem LO.FirstOrder.Arithmetic.computable_iff_sigma1 {f : ℕ → ℕ} : Computable f ↔ 𝚺₁-Function₁ f

theorem LO.FirstOrder.Arithmetic.computable₂_iff_sigma1 {f : ℕ → ℕ → ℕ} : Computable₂ f ↔ 𝚺₁-Function₂ f