structure LO.FirstOrder.Arith.LDef : Type

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

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

• Func : V → V → Prop
• Rel : V → V → Prop

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

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

Instances

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

theorem LO.Arith.Language.Defined.func {V : Type u_1} [LO.ORingStruc V] {L : LO.Arith.Language V} {pL : outParam LO.FirstOrder.Arith.LDef} [self : L.Defined pL] : 𝚺₀-Relation L.Func via pL.func

theorem LO.Arith.Language.Defined.rel {V : Type u_1} [LO.ORingStruc V] {L : LO.Arith.Language V} {pL : outParam LO.FirstOrder.Arith.LDef} [self : L.Defined pL] : 𝚺₀-Relation L.Rel via pL.rel

@[simp]

theorem LO.Arith.Language.Defined.eval_func {V : Type u_1} [LO.ORingStruc V] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (v : Fin 2 → V) : V ⊧/v (LO.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} [LO.ORingStruc V] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val pL.rel) ↔ L.Rel (v 0) (v 1)

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

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

Equations

• ⋯ = ⋯

@[simp]

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

Equations

• ⋯ = ⋯

instance LO.Arith.instGoedelNumberFunc_arithmetization {L₀ : LO.FirstOrder.Language} [L₀.ORing] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] (k : ℕ) : LO.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₀ : LO.FirstOrder.Language} [L₀.ORing] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Rel k)] (k : ℕ) : LO.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 : LO.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] (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val (LO.Arith.DefinableLanguage.toLDef L).func)
• rel_iff : ∀ {k c : ℕ}, c ∈ Set.range Encodable.encode ↔ ℕ ⊧/![k, c] (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val (LO.Arith.DefinableLanguage.toLDef L).rel)

Instances

• LO.Arith.instDefinableLanguageORing

theorem LO.Arith.DefinableLanguage.func_iff {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [self : LO.Arith.DefinableLanguage L] {k : ℕ} {c : ℕ} : c ∈ Set.range Encodable.encode ↔ ℕ ⊧/![k, c] (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val (LO.Arith.DefinableLanguage.toLDef L).func)

theorem LO.Arith.DefinableLanguage.rel_iff {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [self : LO.Arith.DefinableLanguage L] {k : ℕ} {c : ℕ} : c ∈ Set.range Encodable.encode ↔ ℕ ⊧/![k, c] (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val (LO.Arith.DefinableLanguage.toLDef L).rel)

def LO.FirstOrder.Language.lDef (L : LO.FirstOrder.Language) [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [d : LO.Arith.DefinableLanguage L] : LO.FirstOrder.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 : LO.FirstOrder.Language) [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (V : Type u_1) [LO.ORingStruc V] : LO.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 : LO.FirstOrder.Language) [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (V : Type u_1) [LO.ORingStruc V] : (L.codeIn V).Func = fun (x y : V) => V ⊧/![x, y] (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val L.lDef.func)

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

Equations

• LO.Arith.instDefinedCodeInLDef = { func := ⋯, rel := ⋯ }

instance LO.Arith.instGoedelQuoteFunc_arithmetization {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} : LO.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 : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Rel k)] {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} : LO.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 : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} (f : L.Func k) : ⌜f⌝ = ↑(Encodable.encode f)

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

theorem LO.Arith.codeIn_func_quote_iff {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {V : Type u_1} [LO.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 : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {V : Type u_1} [LO.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 : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} (f : L.Func k) : (L.codeIn V).Func ↑k ⌜f⌝

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.Arith.coe_quote_rel_nat {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Rel k)] {V : Type u_1} [LO.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 : LO.Arith.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} [LO.ORingStruc V] : LO.Arith.Language V

Equations

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

Instances For

• LO.Arith.Formalized.LOR.defined

@[reducible, inline]

abbrev LO.Arith.Formalized.LOR.code : LO.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) [LO.ORingStruc V] : ⌜ℒₒᵣ⌝.Defined ℒₒᵣ.lDef

Equations

• LO.Arith.Formalized.LOR.defined V = inferInstance

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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : ⌜ℒₒᵣ⌝.Func 0 ↑LO.Arith.Formalized.zeroIndex

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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