Instances For
class
LO.Arith.Language.Defined
{V : Type u_1}
[LO.ORingStruc V]
(L : LO.Arith.Language V)
(pL : outParam LO.FirstOrder.Arith.LDef)
:
Instances
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]
:
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]
:
@[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]
:
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]
:
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
:
- 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
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]
:
Equations
- L.lDef = LO.Arith.DefinableLanguage.toLDef L
Instances For
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]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
:
@[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)
:
@[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)
:
@[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)
:
Equations
- One or more equations did not get rendered due to their size.
@[reducible, inline]
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Arith.Formalized.«term⌜ℒₒᵣ⌝» = Lean.ParserDescr.node `LO.Arith.Formalized.term⌜ℒₒᵣ⌝ 1024 (Lean.ParserDescr.symbol "⌜ℒₒᵣ⌝")
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- LO.Arith.Formalized.«termP⌜ℒₒᵣ⌝» = Lean.ParserDescr.node `LO.Arith.Formalized.termP⌜ℒₒᵣ⌝ 1024 (Lean.ParserDescr.symbol "p⌜ℒₒᵣ⌝")
Instances For
Equations
- LO.Arith.Formalized.LOR.defined V = inferInstance
Equations
- LO.Arith.Formalized.zeroIndex = Encodable.encode LO.FirstOrder.Language.Zero.zero
Instances For
Equations
- LO.Arith.Formalized.oneIndex = Encodable.encode LO.FirstOrder.Language.One.one
Instances For
Equations
- LO.Arith.Formalized.addIndex = Encodable.encode LO.FirstOrder.Language.Add.add
Instances For
Equations
- LO.Arith.Formalized.mulIndex = Encodable.encode LO.FirstOrder.Language.Mul.mul
Instances For
Equations
Instances For
Equations
Instances For
@[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))))”)
⋯