Arithmetization.ISigmaOne.Metamath.Language

source

structure LO.FirstOrder.Arith.LDef :

Type

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

Instances For

source

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

Type u_1

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

Instances For

source

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

source

@[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)

source

@[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)

source

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

source

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

source

@[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

source

@[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

source

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

source

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

source

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

source

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

source

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

source

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)

source

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

source

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

source

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

source

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)

source

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)

source

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

source

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

source

@[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⌝

source

@[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⌝

source

@[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₂

source

@[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₂

source

@[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⌝

source

@[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⌝

source

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

source

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

source

instance LO.Arith.instDefinableLanguageORing :

DefinableLanguage ℒₒᵣ

Equations

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

source

@[reducible, inline]

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

Arith.Language V

Equations

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

Instances For

source

@[reducible, inline]

abbrev LO.Arith.Formalized.LOR.code :

FirstOrder.Arith.LDef

Equations

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

Instances For

source

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

Lean.ParserDescr

Equations

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

Instances For

source

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

Lean.ParserDescr

Equations

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

Instances For

source

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

Lean.ParserDescr

Equations

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

Instances For

source

instance LO.Arith.Formalized.LOR.defined (V : Type u_1) [ORingStruc V] :

⌜ℒₒᵣ⌝.Defined ℒₒᵣ.lDef

source

def LO.Arith.Formalized.zeroIndex :

ℕ

Equations

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

Instances For

source

def LO.Arith.Formalized.oneIndex :

ℕ

Equations

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

Instances For

source

def LO.Arith.Formalized.addIndex :

ℕ

Equations

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

Instances For

source

def LO.Arith.Formalized.mulIndex :

ℕ

Equations

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

Instances For

source

def LO.Arith.Formalized.eqIndex :

ℕ

Equations

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

Instances For

source

def LO.Arith.Formalized.ltIndex :

ℕ

Equations

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

Instances For

source

@[simp]

theorem LO.Arith.Formalized.LOR_func_zeroIndex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

⌜ℒₒᵣ⌝.Func 0 ↑zeroIndex

source

@[simp]

theorem LO.Arith.Formalized.LOR_func_oneIndex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

⌜ℒₒᵣ⌝.Func 0 ↑oneIndex

source

@[simp]

theorem LO.Arith.Formalized.LOR_func_addIndex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

⌜ℒₒᵣ⌝.Func 2 ↑addIndex

source

@[simp]

theorem LO.Arith.Formalized.LOR_func_mulIndex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

⌜ℒₒᵣ⌝.Func 2 ↑mulIndex

source

@[simp]

theorem LO.Arith.Formalized.LOR_rel_eqIndex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

⌜ℒₒᵣ⌝.Rel 2 ↑eqIndex

source

@[simp]

theorem LO.Arith.Formalized.LOR_rel_ltIndex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

⌜ℒₒᵣ⌝.Rel 2 ↑ltIndex

source

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

source

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

↑zeroIndex = 0

source

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

↑oneIndex = 1

source

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

↑addIndex = 0

source

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

↑mulIndex = 1

source

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