Representation

theorem Part.unit_dom_iff (x : Part Unit) : x.Dom ↔ () ∈ x

theorem Mathlib.List.Vector.cons_get {α : Type u_1} {k : ℕ} (a : α) (v : List.Vector α k) : (a ::ᵥ v).get = a :> v.get

theorem Nat.Partrec.projection {f : ℕ →. ℕ} (hf : Nat.Partrec f) (unif : ∀ {m n₁ n₂ a₁ a₂ : ℕ}, a₁ ∈ f (Nat.pair m n₁) → a₂ ∈ f (Nat.pair m n₂) → a₁ = a₂) : ∃ (g : ℕ →. ℕ), Nat.Partrec g ∧ ∀ (a m : ℕ), a ∈ g m ↔ ∃ (z : ℕ), a ∈ f (Nat.pair m z)

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₂) : ∃ (g : α →. γ), Partrec g ∧ ∀ (c : γ) (a : α), c ∈ g a ↔ ∃ (b : β), c ∈ f a b

@[reducible, inline]

abbrev RePred {α : Type u_1} [Primcodable α] (p : α → Prop) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• RePred p = REPred p

@[simp]

theorem RePred.const {α : Type u_1} [Primcodable α] (p : Prop) : RePred fun (x : α) => p

theorem RePred.iff {α : Type u_1} [Primcodable α] {p : α → Prop} : RePred p ↔ ∃ (f : α →. Unit), Partrec f ∧ p = fun (x : α) => (f x).Dom

theorem RePred.iff' {α : Type u_1} [Primcodable α] {p : α → Prop} : RePred p ↔ ∃ (f : α →. Unit), Partrec f ∧ ∀ (x : α), p x ↔ (f x).Dom

theorem RePred.and {α : Type u_1} [Primcodable α] {p q : α → Prop} (hp : RePred p) (hq : RePred q) : RePred fun (x : α) => p x ∧ q x

theorem RePred.or {α : Type u_1} [Primcodable α] {p q : α → Prop} (hp : RePred p) (hq : RePred q) : RePred fun (x : α) => p x ∨ q x

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 : Semiterm ℒₒᵣ ξ k) : Primrec fun (v : List.Vector ℕ k) => Semiterm.valm ℕ v.get f t

theorem LO.FirstOrder.Arith.sigma1_re {ξ : Type u_1} (ε : ξ → ℕ) {k : ℕ} {φ : Semiformula ℒₒᵣ ξ k} (hp : Hierarchy Sg 1 φ) : RePred fun (v : List.Vector ℕ k) => (Semiformula.Evalm ℕ v.get ε) φ

def LO.FirstOrder.Arith.codeAux {k : ℕ} : Nat.ArithPart₁.Code k → Formula ℒₒᵣ (Fin (k + 1))

Imported declaration from the Incompleteness formalization.

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)”)

def LO.FirstOrder.Arith.code {k : ℕ} (c : Nat.ArithPart₁.Code k) : Semisentence ℒₒᵣ (k + 1)

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

@[simp]

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

theorem LO.FirstOrder.Arith.models_code {k : ℕ} {c : Nat.ArithPart₁.Code k} {f : List.Vector ℕ k →. ℕ} (hc : c.eval f) (y : ℕ) (v : Fin k → ℕ) : ℕ ⊧/(y :> v) (code c) ↔ y ∈ f (List.Vector.ofFn v)

noncomputable def LO.FirstOrder.Arith.codeOfPartrec' {k : ℕ} (f : List.Vector ℕ k →. ℕ) : Semisentence ℒₒᵣ (k + 1)

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.FirstOrder.Arith.codeOfPartrec'_spec {k : ℕ} {f : List.Vector ℕ k →. ℕ} (hf : Nat.Partrec' f) {y : ℕ} {v : Fin k → ℕ} : ℕ ⊧/(y :> v) (codeOfPartrec' f) ↔ y ∈ f (List.Vector.ofFn v)

noncomputable def LO.FirstOrder.Arith.codeOfRePred (p : ℕ → Prop) : Semisentence ℒₒᵣ 1

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.FirstOrder.Arith.codeOfRePred_spec {p : ℕ → Prop} (hp : RePred p) {x : ℕ} : ℕ ⊧/![x] (codeOfRePred p) ↔ p x

theorem LO.FirstOrder.Arith.re_complete {T : Theory ℒₒᵣ} [𝐑₀ wkn T] [Sigma1Sound T] {p : ℕ → Prop} (hp : RePred p) {x : ℕ} : p x ↔ T ⊢! ↑((codeOfRePred p)/[↑x])