Equations
- termExp_ = Lean.ParserDescr.node `termExp_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "exp ") (Lean.ParserDescr.cat `term 90))
Instances For
Equations
- instToStringEmpty_arithmetization = { toString := Empty.elim }
Equations
- «term_#_» = Lean.ParserDescr.trailingNode `term_#_ 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " # ") (Lean.ParserDescr.cat `term 81))
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- x.coe = match x with | LO.Polarity.sigma => 𝚺 | LO.Polarity.pi => 𝚷
Instances For
Equations
- LO.Polarity.instCoe_arithmetization = { coe := LO.Polarity.coe }
@[simp]
@[simp]
def
LO.FirstOrder.Arith.termToStr
{μ : Type u_1}
[ToString μ]
{n : ℕ}
:
LO.FirstOrder.Semiterm ℒₒᵣ μ n → String
Equations
- One or more equations did not get rendered due to their size.
- LO.FirstOrder.Arith.termToStr (LO.FirstOrder.Semiterm.bvar x_1) = "x_{" ++ toString (n - 1 - ↑x_1) ++ "}"
- LO.FirstOrder.Arith.termToStr (LO.FirstOrder.Semiterm.fvar x_1) = "a_{" ++ toString x_1 ++ "}"
- LO.FirstOrder.Arith.termToStr (LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.ORing.Func.zero a) = "0"
- LO.FirstOrder.Arith.termToStr (LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.ORing.Func.one a) = "1"
Instances For
instance
LO.FirstOrder.Arith.instReprSemitermORing_arithmetization
{μ : Type u_1}
[ToString μ]
{n : ℕ}
:
Repr (LO.FirstOrder.Semiterm ℒₒᵣ μ n)
Equations
- LO.FirstOrder.Arith.instReprSemitermORing_arithmetization = { reprPrec := fun (t : LO.FirstOrder.Semiterm ℒₒᵣ μ n) (x : ℕ) => Std.Format.text (LO.FirstOrder.Arith.termToStr t) }
instance
LO.FirstOrder.Arith.instToStringSemitermORing_arithmetization
{μ : Type u_1}
[ToString μ]
{n : ℕ}
:
Equations
- LO.FirstOrder.Arith.instToStringSemitermORing_arithmetization = { toString := LO.FirstOrder.Arith.termToStr }
Instances For
instance
LO.FirstOrder.Arith.instReprSemiformulaORing_arithmetization
{μ : Type u_1}
[ToString μ]
{n : ℕ}
:
Repr (LO.FirstOrder.Semiformula ℒₒᵣ μ n)
Equations
- LO.FirstOrder.Arith.instReprSemiformulaORing_arithmetization = { reprPrec := fun (t : LO.FirstOrder.Semiformula ℒₒᵣ μ n) (x : ℕ) => Std.Format.text (LO.FirstOrder.Arith.formulaToStr t) }
instance
LO.FirstOrder.Arith.instToStringSemiformulaORing_arithmetization
{μ : Type u_1}
[ToString μ]
{n : ℕ}
:
Equations
- LO.FirstOrder.Arith.instToStringSemiformulaORing_arithmetization = { toString := LO.FirstOrder.Arith.formulaToStr }
instance
LO.FirstOrder.Arith.indScheme_of_indH
(M : Type u_1)
[LO.ORingStruc M]
(Γ : LO.Polarity)
(n : ℕ)
[M ⊧ₘ* 𝐈𝐍𝐃Γ n]
:
Equations
- ⋯ = ⋯
@[simp]
theorem
LO.FirstOrder.Semiformula.eval_operator₃
{ξ : Type u_3}
{L : LO.FirstOrder.Language}
{M : Type u_1}
{s : LO.FirstOrder.Structure L M}
{n : ℕ}
{ε : ξ → M}
{e : Fin n → M}
{o : LO.FirstOrder.Semiformula.Operator L 3}
{t₁ : LO.FirstOrder.Semiterm L ξ n}
{t₂ : LO.FirstOrder.Semiterm L ξ n}
{t₃ : LO.FirstOrder.Semiterm L ξ n}
:
(LO.FirstOrder.Semiformula.Eval s e ε) (o.operator ![t₁, t₂, t₃]) ↔ o.val ![LO.FirstOrder.Semiterm.val s e ε t₁, LO.FirstOrder.Semiterm.val s e ε t₂, LO.FirstOrder.Semiterm.val s e ε t₃]
@[simp]
theorem
LO.FirstOrder.Semiformula.eval_operator₄
{ξ : Type u_3}
{L : LO.FirstOrder.Language}
{M : Type u_1}
{s : LO.FirstOrder.Structure L M}
{n : ℕ}
{ε : ξ → M}
{e : Fin n → M}
{o : LO.FirstOrder.Semiformula.Operator L 4}
{t₁ : LO.FirstOrder.Semiterm L ξ n}
{t₂ : LO.FirstOrder.Semiterm L ξ n}
{t₃ : LO.FirstOrder.Semiterm L ξ n}
{t₄ : LO.FirstOrder.Semiterm L ξ n}
:
(LO.FirstOrder.Semiformula.Eval s e ε) (o.operator ![t₁, t₂, t₃, t₄]) ↔ o.val
![LO.FirstOrder.Semiterm.val s e ε t₁, LO.FirstOrder.Semiterm.val s e ε t₂, LO.FirstOrder.Semiterm.val s e ε t₃,
LO.FirstOrder.Semiterm.val s e ε t₄]
@[reducible, inline]
abbrev
LO.FirstOrder.Semiterm.Rlz
{L : LO.FirstOrder.Language}
{M : Type u_1}
[LO.FirstOrder.Structure L M]
{n : ℕ}
(t : LO.FirstOrder.Semiterm L M n)
(e : Fin n → M)
:
M
Equations
- t.Rlz e = LO.FirstOrder.Semiterm.valm M e id t
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Semiformula.Rlz
{L : LO.FirstOrder.Language}
{M : Type u_1}
[LO.FirstOrder.Structure L M]
{n : ℕ}
(p : LO.FirstOrder.Semiformula L M n)
(e : Fin n → M)
:
Equations
- p.Rlz e = (LO.FirstOrder.Semiformula.Evalm M e id) p
Instances For
@[simp]
theorem
LO.FirstOrder.models₀_not_iff
{L : LO.FirstOrder.Language}
{M : Type u_1}
[Nonempty M]
[LO.FirstOrder.Structure L M]
(σ : LO.FirstOrder.Sentence L)
:
@[simp]
theorem
LO.FirstOrder.models₀_or_iff
{L : LO.FirstOrder.Language}
{M : Type u_1}
[Nonempty M]
[LO.FirstOrder.Structure L M]
(σ : LO.FirstOrder.Sentence L)
(π : LO.FirstOrder.Sentence L)
:
@[simp]
theorem
LO.FirstOrder.models₀_imply_iff
{L : LO.FirstOrder.Language}
{M : Type u_1}
[Nonempty M]
[LO.FirstOrder.Structure L M]
(σ : LO.FirstOrder.Sentence L)
(π : LO.FirstOrder.Sentence L)
:
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.exItr
{L : LO.FirstOrder.Language}
[L.LT]
{μ : Type v}
{s : ℕ}
{n : ℕ}
{k : ℕ}
{p : LO.FirstOrder.Semiformula L μ (n + k)}
:
LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1) (∃^[k] p) ↔ LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1) p
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.univItr
{L : LO.FirstOrder.Language}
[L.LT]
{μ : Type v}
{s : ℕ}
{n : ℕ}
{k : ℕ}
{p : LO.FirstOrder.Semiformula L μ (n + k)}
:
LO.FirstOrder.Arith.Hierarchy 𝚷 (s + 1) (∀^[k] p) ↔ LO.FirstOrder.Arith.Hierarchy 𝚷 (s + 1) p
instance
LO.FirstOrder.Arith.instModelsTheoryCobhamR0_arithmetization
(M : Type u_1)
[LO.ORingStruc M]
[M ⊧ₘ* 𝐏𝐀⁻]
:
Equations
- ⋯ = ⋯
theorem
LO.FirstOrder.Arith.nat_extention_sigmaOne
(M : Type u_1)
[LO.ORingStruc M]
[M ⊧ₘ* 𝐏𝐀⁻]
{σ : LO.FirstOrder.Sentence ℒₒᵣ}
(hσ : LO.FirstOrder.Arith.Hierarchy 𝚺 1 σ)
:
theorem
LO.FirstOrder.Arith.nat_extention_piOne
(M : Type u_1)
[LO.ORingStruc M]
[M ⊧ₘ* 𝐏𝐀⁻]
{σ : LO.FirstOrder.Sentence ℒₒᵣ}
(hσ : LO.FirstOrder.Arith.Hierarchy 𝚷 1 σ)
:
theorem
LO.Arith.bold_sigma_one_completeness'
{M : Type u_1}
[LO.ORingStruc M]
[M ⊧ₘ* 𝐑₀]
{n : ℕ}
{σ : LO.FirstOrder.Semisentence ℒₒᵣ n}
(hσ : LO.FirstOrder.Arith.Hierarchy 𝚺 1 σ)
{e : Fin n → ℕ}
:
ℕ ⊧/e σ → (M ⊧/fun (x : Fin n) => LO.ORingStruc.numeral (e x)) σ