theorem
Partrec.projection
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable γ]
{f : α → β →. γ}
(hf : Partrec₂ f)
(unif : ∀ {a : α} {b₁ b₂ : β} {c₁ c₂ : γ}, c₁ ∈ f a b₁ → c₂ ∈ f a b₂ → c₁ = c₂)
:
@[simp]
theorem
RePred.and
{α : Type u_1}
[Primcodable α]
{p : α → Prop}
{q : α → Prop}
(hp : RePred p)
(hq : RePred q)
:
theorem
RePred.projection
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{p : α × β → Prop}
(hp : RePred p)
:
RePred fun (x : α) => ∃ (y : β), p (x, y)
theorem
RePred.comp
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{f : α → β}
(hf : Computable f)
{p : β → Prop}
(hp : RePred p)
:
RePred fun (x : α) => p (f x)
theorem
LO.FirstOrder.Arith.term_primrec
{ξ : Type u_1}
{k : ℕ}
{f : ξ → ℕ}
(t : LO.FirstOrder.Semiterm ℒₒᵣ ξ k)
:
Primrec fun (v : Mathlib.Vector ℕ k) => LO.FirstOrder.Semiterm.valm ℕ v.get f t
theorem
LO.FirstOrder.Arith.sigma1_re
{ξ : Type u_1}
(ε : ξ → ℕ)
{k : ℕ}
{p : LO.FirstOrder.Semiformula ℒₒᵣ ξ k}
(hp : LO.FirstOrder.Arith.Hierarchy 𝚺 1 p)
:
RePred fun (v : Mathlib.Vector ℕ k) => (LO.FirstOrder.Semiformula.Evalm ℕ v.get ε) p
def
LO.FirstOrder.Arith.codeAux
{k : ℕ}
:
Nat.ArithPart₁.Code k → LO.FirstOrder.Formula ℒₒᵣ (Fin (k + 1))
Equations
- One or more equations did not get rendered due to their size.
- LO.FirstOrder.Arith.codeAux (Nat.ArithPart₁.Code.zero x) = (“!!(LO.FirstOrder.Semiterm.fvar 0) = 0”)
- LO.FirstOrder.Arith.codeAux (Nat.ArithPart₁.Code.one x) = (“!!(LO.FirstOrder.Semiterm.fvar 0) = 1”)
- LO.FirstOrder.Arith.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.Arith.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.Arith.codeAux (Nat.ArithPart₁.Code.proj i) = (“!!(LO.FirstOrder.Semiterm.fvar 0) = !!(LO.FirstOrder.Semiterm.fvar i.succ)”)
Instances For
def
LO.FirstOrder.Arith.code
{k : ℕ}
(c : Nat.ArithPart₁.Code k)
:
LO.FirstOrder.Semisentence ℒₒᵣ (k + 1)
Equations
- LO.FirstOrder.Arith.code c = (LO.FirstOrder.Rew.bind ![] (LO.FirstOrder.Semiterm.bvar 0 :> fun (x : Fin k) => LO.FirstOrder.Semiterm.bvar x.succ)).hom (LO.FirstOrder.Arith.codeAux c)
Instances For
@[simp]
theorem
LO.FirstOrder.Arith.models_code
{k : ℕ}
{c : Nat.ArithPart₁.Code k}
{f : Mathlib.Vector ℕ k →. ℕ}
(hc : c.eval f)
(y : ℕ)
(v : Fin k → ℕ)
:
ℕ ⊧/(y :> v) (LO.FirstOrder.Arith.code c) ↔ y ∈ f (Mathlib.Vector.ofFn v)
noncomputable def
LO.FirstOrder.Arith.codeOfPartrec'
{k : ℕ}
(f : Mathlib.Vector ℕ k →. ℕ)
:
LO.FirstOrder.Semisentence ℒₒᵣ (k + 1)
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.FirstOrder.Arith.codeOfPartrec'_spec
{k : ℕ}
{f : Mathlib.Vector ℕ k →. ℕ}
(hf : Nat.Partrec' f)
{y : ℕ}
{v : Fin k → ℕ}
:
ℕ ⊧/(y :> v) (LO.FirstOrder.Arith.codeOfPartrec' f) ↔ y ∈ f (Mathlib.Vector.ofFn v)
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.FirstOrder.Arith.codeOfRePred_spec
{p : ℕ → Prop}
(hp : RePred p)
{x : ℕ}
:
ℕ ⊧/![x] (LO.FirstOrder.Arith.codeOfRePred p) ↔ p x
theorem
LO.FirstOrder.Arith.re_complete
{T : LO.FirstOrder.Theory ℒₒᵣ}
[𝐑₀ ≼ T]
[LO.FirstOrder.Arith.Sigma1Sound T]
{p : ℕ → Prop}
(hp : RePred p)
{x : ℕ}
: