structure LO.FirstOrder.Arith.LDef : Type

• func : 𝚺₀.Semisentence 2
• rel : 𝚺₀.Semisentence 2

structure LO.Arith.Language (V : Type u_1) : Type u_1

• Func (arity : V) : V → Prop
• Rel (arity : V) : V → Prop

class LO.Arith.Language.Defined {V : Type u_1} [ORingStruc V] (L : Arith.Language V) (pL : outParam FirstOrder.Arith.LDef) : Prop

• func : 𝚺₀-Relation L.Func via pL.func
• rel : 𝚺₀-Relation L.Rel via pL.rel

Instances

• LO.Arith.Formalized.LOR.defined
• LO.Arith.instDefinedCodeInLDef

@[simp]

theorem LO.Arith.Language.Defined.eval_func {V : Type u_1} [ORingStruc V] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (v : Fin 2 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val pL.func) ↔ L.Func (v 0) (v 1)

@[simp]

theorem LO.Arith.Language.Defined.eval_rel_iff {V : Type u_1} [ORingStruc V] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (v : Fin 2 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val pL.rel) ↔ L.Rel (v 0) (v 1)

instance LO.Arith.Language.Defined.func_definable {V : Type u_1} [ORingStruc V] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] : 𝚺₀-Relation L.Func

instance LO.Arith.Language.Defined.rel_definable {V : Type u_1} [ORingStruc V] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] : 𝚺₀-Relation L.Rel

@[simp]

instance LO.Arith.Language.Defined.func_definable' {V : Type u_1} [ORingStruc V] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (ℌ : FirstOrder.Arith.HierarchySymbol) : ℌ-Relation L.Func

@[simp]

instance LO.Arith.Language.Defined.rel_definable' {V : Type u_1} [ORingStruc V] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (ℌ : FirstOrder.Arith.HierarchySymbol) : ℌ-Relation L.Rel

instance LO.Arith.instGoedelNumberFunc_arithmetization {L₀ : FirstOrder.Language} [L₀.ORing] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] (k : ℕ) : FirstOrder.Semiterm.Operator.GoedelNumber L₀ (L.Func k)

Equations

• LO.Arith.instGoedelNumberFunc_arithmetization k = { goedelNumber := fun (f : L.Func k) => LO.FirstOrder.Semiterm.Operator.numeral L₀ (Encodable.encode f) }

instance LO.Arith.instGoedelNumberRel_arithmetization {L₀ : FirstOrder.Language} [L₀.ORing] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Rel k)] (k : ℕ) : FirstOrder.Semiterm.Operator.GoedelNumber L₀ (L.Rel k)

Equations

• LO.Arith.instGoedelNumberRel_arithmetization k = { goedelNumber := fun (r : L.Rel k) => LO.FirstOrder.Semiterm.Operator.numeral L₀ (Encodable.encode r) }

class LO.Arith.DefinableLanguage (L : FirstOrder.Language) [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] extends LO.FirstOrder.Arith.LDef : Type

• func : 𝚺₀.Semisentence 2
• rel : 𝚺₀.Semisentence 2
• func_iff {k c : ℕ} : c ∈ Set.range Encodable.encode ↔ ℕ ⊧/![k, c] (FirstOrder.Arith.HierarchySymbol.Semiformula.val (toLDef L).func)
• rel_iff {k c : ℕ} : c ∈ Set.range Encodable.encode ↔ ℕ ⊧/![k, c] (FirstOrder.Arith.HierarchySymbol.Semiformula.val (toLDef L).rel)

Instances

• LO.Arith.instDefinableLanguageORing

def LO.FirstOrder.Language.lDef (L : Language) [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [d : Arith.DefinableLanguage L] : Arith.LDef

Equations

• L.lDef = LO.Arith.DefinableLanguage.toLDef L

Instances For

• LO.Arith.Formalized.LOR.defined
• LO.Arith.instDefinedCodeInLDef

def LO.FirstOrder.Language.codeIn (L : Language) [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] (V : Type u_1) [ORingStruc V] : Arith.Language V

Equations

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

Instances For

• LO.Arith.instDefinedCodeInLDef

theorem LO.FirstOrder.Language.codeIn_func_def (L : Language) [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] (V : Type u_1) [ORingStruc V] : (L.codeIn V).Func = fun (x y : V) => V ⊧/![x, y] (Arith.HierarchySymbol.Semiformula.val L.lDef.func)

instance LO.Arith.instDefinedCodeInLDef {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {V : Type u_1} [ORingStruc V] : (L.codeIn V).Defined L.lDef

instance LO.Arith.instGoedelQuoteFunc_arithmetization {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} : GoedelQuote (L.Func k) V

Equations

• LO.Arith.instGoedelQuoteFunc_arithmetization = { quote := fun (f : L.Func k) => ↑(Encodable.encode f) }

instance LO.Arith.instGoedelQuoteRel_arithmetization {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Rel k)] {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} : GoedelQuote (L.Rel k) V

Equations

• LO.Arith.instGoedelQuoteRel_arithmetization = { quote := fun (R : L.Rel k) => ↑(Encodable.encode R) }

theorem LO.Arith.quote_func_def {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} (f : L.Func k) : ⌜f⌝ = ↑(Encodable.encode f)

theorem LO.Arith.quote_rel_def {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Rel k)] {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} (R : L.Rel k) : ⌜R⌝ = ↑(Encodable.encode R)

theorem LO.Arith.codeIn_func_quote_iff {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k x : ℕ} : (L.codeIn V).Func ↑k ↑x ↔ ∃ (f : L.Func k), Encodable.encode f = x

theorem LO.Arith.codeIn_rel_quote_iff {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k x : ℕ} : (L.codeIn V).Rel ↑k ↑x ↔ ∃ (R : L.Rel k), Encodable.encode R = x

@[simp]

theorem LO.Arith.codeIn_func_quote {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} (f : L.Func k) : (L.codeIn V).Func ↑k ⌜f⌝

@[simp]

theorem LO.Arith.codeIn_rel_quote {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} (r : L.Rel k) : (L.codeIn V).Rel ↑k ⌜r⌝

@[simp]

theorem LO.Arith.quote_func_inj {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} (f₁ f₂ : L.Func k) : ⌜f₁⌝ = ⌜f₂⌝ ↔ f₁ = f₂

@[simp]

theorem LO.Arith.quote_rel_inj {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Rel k)] {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} (R₁ R₂ : L.Rel k) : ⌜R₁⌝ = ⌜R₂⌝ ↔ R₁ = R₂

@[simp]

theorem LO.Arith.coe_quote_func_nat {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} (f : L.Func k) : ↑⌜f⌝ = ⌜f⌝

@[simp]

theorem LO.Arith.coe_quote_rel_nat {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Rel k)] {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} (R : L.Rel k) : ↑⌜R⌝ = ⌜R⌝

theorem LO.FirstOrder.Language.ORing.of_mem_range_encode_func {k f : ℕ} : f ∈ Set.range Encodable.encode ↔ k = 0 ∧ f = 0 ∨ k = 0 ∧ f = 1 ∨ k = 2 ∧ f = 0 ∨ k = 2 ∧ f = 1

TODO: move to Basic/Syntax/Language.lean

theorem LO.FirstOrder.Language.ORing.of_mem_range_encode_rel {k r : ℕ} : r ∈ Set.range Encodable.encode ↔ k = 2 ∧ r = 0 ∨ k = 2 ∧ r = 1

TODO: move to Basic/Syntax/Language.lean

instance LO.Arith.instDefinableLanguageORing : DefinableLanguage ℒₒᵣ

Equations

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

@[reducible, inline]

abbrev LO.Arith.Formalized.LOR {V : Type u_1} [ORingStruc V] : Arith.Language V

Equations

• ⌜ℒₒᵣ⌝ = ℒₒᵣ.codeIn V

Instances For

• LO.Arith.Formalized.LOR.defined

@[reducible, inline]

abbrev LO.Arith.Formalized.LOR.code : FirstOrder.Arith.LDef

Equations

• p⌜ℒₒᵣ⌝ = ℒₒᵣ.lDef

def LO.Arith.Formalized.«term⌜ℒₒᵣ⌝» : Lean.ParserDescr

Equations

• LO.Arith.Formalized.«term⌜ℒₒᵣ⌝» = Lean.ParserDescr.node `LO.Arith.Formalized.«term⌜ℒₒᵣ⌝» 1024 (Lean.ParserDescr.symbol "⌜ℒₒᵣ⌝")

def LO.Arith.Formalized.«term⌜ℒₒᵣ⌝[_]» : Lean.ParserDescr

Equations

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

def LO.Arith.Formalized.«termP⌜ℒₒᵣ⌝» : Lean.ParserDescr

Equations

• LO.Arith.Formalized.«termP⌜ℒₒᵣ⌝» = Lean.ParserDescr.node `LO.Arith.Formalized.«termP⌜ℒₒᵣ⌝» 1024 (Lean.ParserDescr.symbol "p⌜ℒₒᵣ⌝")

instance LO.Arith.Formalized.LOR.defined (V : Type u_1) [ORingStruc V] : ⌜ℒₒᵣ⌝.Defined ℒₒᵣ.lDef

def LO.Arith.Formalized.zeroIndex : ℕ

Equations

• LO.Arith.Formalized.zeroIndex = Encodable.encode LO.FirstOrder.Language.Zero.zero

def LO.Arith.Formalized.oneIndex : ℕ

Equations

• LO.Arith.Formalized.oneIndex = Encodable.encode LO.FirstOrder.Language.One.one

def LO.Arith.Formalized.addIndex : ℕ

Equations

• LO.Arith.Formalized.addIndex = Encodable.encode LO.FirstOrder.Language.Add.add

def LO.Arith.Formalized.mulIndex : ℕ

Equations

• LO.Arith.Formalized.mulIndex = Encodable.encode LO.FirstOrder.Language.Mul.mul

def LO.Arith.Formalized.eqIndex : ℕ

Equations

• LO.Arith.Formalized.eqIndex = Encodable.encode op(=)

def LO.Arith.Formalized.ltIndex : ℕ

Equations

• LO.Arith.Formalized.ltIndex = Encodable.encode op(<)

@[simp]

theorem LO.Arith.Formalized.LOR_func_zeroIndex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : ⌜ℒₒᵣ⌝.Func 0 ↑zeroIndex

@[simp]

theorem LO.Arith.Formalized.LOR_func_oneIndex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : ⌜ℒₒᵣ⌝.Func 0 ↑oneIndex

@[simp]

theorem LO.Arith.Formalized.LOR_func_addIndex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : ⌜ℒₒᵣ⌝.Func 2 ↑addIndex

@[simp]

theorem LO.Arith.Formalized.LOR_func_mulIndex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : ⌜ℒₒᵣ⌝.Func 2 ↑mulIndex

@[simp]

theorem LO.Arith.Formalized.LOR_rel_eqIndex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : ⌜ℒₒᵣ⌝.Rel 2 ↑eqIndex

@[simp]

theorem LO.Arith.Formalized.LOR_rel_ltIndex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : ⌜ℒₒᵣ⌝.Rel 2 ↑ltIndex

theorem LO.Arith.Formalized.lDef.func_def : ℒₒᵣ.lDef.func = FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma (“((!!(FirstOrder.Semiterm.bvar 0) = !!↑0 ∧ !!(FirstOrder.Semiterm.bvar 1) = !!↑0) ∨ ((!!(FirstOrder.Semiterm.bvar 0) = !!↑0 ∧ !!(FirstOrder.Semiterm.bvar 1) = !!↑1) ∨ ((!!(FirstOrder.Semiterm.bvar 0) = !!↑2 ∧ !!(FirstOrder.Semiterm.bvar 1) = !!↑0) ∨ (!!(FirstOrder.Semiterm.bvar 0) = !!↑2 ∧ !!(FirstOrder.Semiterm.bvar 1) = !!↑1))))”) ⋯

theorem LO.Arith.Formalized.coe_zeroIndex_eq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : ↑zeroIndex = 0

theorem LO.Arith.Formalized.coe_oneIndex_eq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : ↑oneIndex = 1

theorem LO.Arith.Formalized.coe_addIndex_eq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : ↑addIndex = 0

theorem LO.Arith.Formalized.coe_mulIndex_eq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : ↑mulIndex = 1

theorem LO.Arith.Formalized.func_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k f : V} : ⌜ℒₒᵣ⌝.Func k f ↔ k = 0 ∧ f = ↑zeroIndex ∨ k = 0 ∧ f = ↑oneIndex ∨ k = 2 ∧ f = ↑addIndex ∨ k = 2 ∧ f = ↑mulIndex