Equations
- LO.ORingStruc.numeral 0 = 0
- LO.ORingStruc.numeral 1 = 1
- LO.ORingStruc.numeral n.succ.succ = LO.ORingStruc.numeral (n + 1) + 1
Instances For
@[simp]
@[simp]
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.FirstOrder.Language.oringEmb_zero
{L : LO.FirstOrder.Language}
[L.ORing]
:
LO.FirstOrder.Language.oringEmb.func LO.FirstOrder.Language.Zero.zero = LO.FirstOrder.Language.Zero.zero
@[simp]
theorem
LO.FirstOrder.Language.oringEmb_one
{L : LO.FirstOrder.Language}
[L.ORing]
:
LO.FirstOrder.Language.oringEmb.func LO.FirstOrder.Language.One.one = LO.FirstOrder.Language.One.one
@[simp]
theorem
LO.FirstOrder.Language.oringEmb_add
{L : LO.FirstOrder.Language}
[L.ORing]
:
LO.FirstOrder.Language.oringEmb.func LO.FirstOrder.Language.Add.add = LO.FirstOrder.Language.Add.add
@[simp]
theorem
LO.FirstOrder.Language.oringEmb_mul
{L : LO.FirstOrder.Language}
[L.ORing]
:
LO.FirstOrder.Language.oringEmb.func LO.FirstOrder.Language.Mul.mul = LO.FirstOrder.Language.Mul.mul
@[simp]
theorem
LO.FirstOrder.Language.oringEmb_eq
{L : LO.FirstOrder.Language}
[L.ORing]
:
LO.FirstOrder.Language.oringEmb.rel op(=) = op(=)
@[simp]
theorem
LO.FirstOrder.Language.oringEmb_lt
{L : LO.FirstOrder.Language}
[L.ORing]
:
LO.FirstOrder.Language.oringEmb.rel op(<) = op(<)
instance
LO.FirstOrder.Semiterm.instCoeORing
{L : LO.FirstOrder.Language}
[L.ORing]
{ξ : Type u_2}
{n : ℕ}
:
Coe (LO.FirstOrder.Semiterm ℒₒᵣ ξ n) (LO.FirstOrder.Semiterm L ξ n)
Equations
- LO.FirstOrder.Semiterm.instCoeORing = { coe := LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb }
@[simp]
theorem
LO.FirstOrder.Semiterm.oringEmb_zero
{L : LO.FirstOrder.Language}
[L.ORing]
{ξ : Type u_1}
{n : ℕ}
:
LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (LO.FirstOrder.Semiterm.Operator.const op(0)) = LO.FirstOrder.Semiterm.Operator.const op(0)
@[simp]
theorem
LO.FirstOrder.Semiterm.oringEmb_one
{L : LO.FirstOrder.Language}
[L.ORing]
{ξ : Type u_1}
{n : ℕ}
:
LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (LO.FirstOrder.Semiterm.Operator.const op(1)) = LO.FirstOrder.Semiterm.Operator.const op(1)
@[simp]
theorem
LO.FirstOrder.Semiterm.oringEmb_add
{L : LO.FirstOrder.Language}
[L.ORing]
{ξ : Type u_1}
{n : ℕ}
(v : Fin 2 → LO.FirstOrder.Semiterm ℒₒᵣ ξ n)
:
LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (op(+).operator v) = (‘(!!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 0)) +
!!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 1)))’)
@[simp]
theorem
LO.FirstOrder.Semiterm.oringEmb_mul
{L : LO.FirstOrder.Language}
[L.ORing]
{ξ : Type u_1}
{n : ℕ}
(v : Fin 2 → LO.FirstOrder.Semiterm ℒₒᵣ ξ n)
:
LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (op(*).operator v) = ‘(!!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 0)) *
!!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 1)))’
@[simp]
theorem
LO.FirstOrder.Semiterm.oringEmb_numeral
{L : LO.FirstOrder.Language}
[L.ORing]
{ξ : Type u_1}
{n : ℕ}
(z : ℕ)
:
LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb
(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ z)) = LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral L z)
instance
LO.FirstOrder.Semiformula.instCoeORing
{L : LO.FirstOrder.Language}
[L.ORing]
{ξ : Type u_2}
{n : ℕ}
:
Coe (LO.FirstOrder.Semiformula ℒₒᵣ ξ n) (LO.FirstOrder.Semiformula L ξ n)
Equations
- LO.FirstOrder.Semiformula.instCoeORing = { coe := ⇑(LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) }
Equations
- LO.FirstOrder.Semiformula.instCoeTheoryORing = { coe := fun (x : LO.FirstOrder.Theory ℒₒᵣ) => ⇑(LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) '' x }
@[simp]
theorem
LO.FirstOrder.Semiformula.oringEmb_eq
{L : LO.FirstOrder.Language}
[L.ORing]
{ξ : Type u_1}
{n : ℕ}
(v : Fin 2 → LO.FirstOrder.Semiterm ℒₒᵣ ξ n)
:
(LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) (op(=).operator v) = (“!!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 0)) =
!!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 1))”)
@[simp]
theorem
LO.FirstOrder.Semiformula.oringEmb_lt
{L : LO.FirstOrder.Language}
[L.ORing]
{ξ : Type u_1}
{n : ℕ}
(v : Fin 2 → LO.FirstOrder.Semiterm ℒₒᵣ ξ n)
:
(LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) (op(<).operator v) = (“!!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 0)) <
!!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 1))”)
@[reducible, inline]
Equations
Instances For
class
LO.FirstOrder.Structure.ORing
(L : LO.FirstOrder.Language)
[L.ORing]
(M : Type w)
[LO.ORingStruc M]
[LO.FirstOrder.Structure L M]
extends
LO.FirstOrder.Structure.Zero
,
LO.FirstOrder.Structure.One
,
LO.FirstOrder.Structure.Add
,
LO.FirstOrder.Structure.Mul
,
LO.FirstOrder.Structure.Eq
,
LO.FirstOrder.Structure.LT
:
Instances
@[simp]
theorem
LO.FirstOrder.Structure.numeral_eq_numeral
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiterm.Operator.Zero L]
[LO.FirstOrder.Semiterm.Operator.One L]
[LO.FirstOrder.Semiterm.Operator.Add L]
{M : Type u}
[LO.ORingStruc M]
[LO.FirstOrder.Structure L M]
[LO.FirstOrder.Structure.Zero L M]
[LO.FirstOrder.Structure.One L M]
[LO.FirstOrder.Structure.Add L M]
(z : ℕ)
:
def
LO.FirstOrder.Semiformula.ballLTSucc
{L : LO.FirstOrder.Language}
[L.LT]
[L.Zero]
[L.One]
[L.Add]
{ξ : Type u_1}
{n : ℕ}
(t : LO.FirstOrder.Semiterm L ξ n)
(p : LO.FirstOrder.Semiformula L ξ (n + 1))
:
Equations
- LO.FirstOrder.Semiformula.ballLTSucc t p = LO.FirstOrder.Semiformula.ballLT (‘(!!t + 1)’) p
Instances For
def
LO.FirstOrder.Semiformula.bexLTSucc
{L : LO.FirstOrder.Language}
[L.LT]
[L.Zero]
[L.One]
[L.Add]
{ξ : Type u_1}
{n : ℕ}
(t : LO.FirstOrder.Semiterm L ξ n)
(p : LO.FirstOrder.Semiformula L ξ (n + 1))
:
Equations
- LO.FirstOrder.Semiformula.bexLTSucc t p = LO.FirstOrder.Semiformula.bexLT (‘(!!t + 1)’) p
Instances For
theorem
LO.FirstOrder.Semiformula.eval_ballLTSucc
{n : ℕ}
{L : LO.FirstOrder.Language}
[L.LT]
[L.Zero]
[L.One]
[L.Add]
{ξ : Type u_1}
{M : Type u_2}
{s : LO.FirstOrder.Structure L M}
[LT M]
[One M]
[Add M]
[LO.FirstOrder.Structure.LT L M]
[LO.FirstOrder.Structure.One L M]
[LO.FirstOrder.Structure.Add L M]
{t : LO.FirstOrder.Semiterm L ξ n}
{p : LO.FirstOrder.Semiformula L ξ (n + 1)}
{e : Fin n → M}
{ε : ξ → M}
:
(LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Semiformula.ballLTSucc t p) ↔ ∀ x < LO.FirstOrder.Semiterm.val s e ε t + 1, (LO.FirstOrder.Semiformula.Eval s (x :> e) ε) p
theorem
LO.FirstOrder.Semiformula.eval_bexLTSucc
{n : ℕ}
{L : LO.FirstOrder.Language}
[L.LT]
[L.Zero]
[L.One]
[L.Add]
{ξ : Type u_1}
{M : Type u_2}
{s : LO.FirstOrder.Structure L M}
[LT M]
[One M]
[Add M]
[LO.FirstOrder.Structure.LT L M]
[LO.FirstOrder.Structure.One L M]
[LO.FirstOrder.Structure.Add L M]
{t : LO.FirstOrder.Semiterm L ξ n}
{p : LO.FirstOrder.Semiformula L ξ (n + 1)}
{e : Fin n → M}
{ε : ξ → M}
:
(LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Semiformula.bexLTSucc t p) ↔ ∃ x < LO.FirstOrder.Semiterm.val s e ε t + 1, (LO.FirstOrder.Semiformula.Eval s (x :> e) ε) p
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
class
LO.FirstOrder.Arith.SoundOn
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Structure L ℕ]
(T : LO.FirstOrder.Theory L)
(F : LO.FirstOrder.SyntacticFormula L → Prop)
:
- sound : ∀ {p : LO.FirstOrder.SyntacticFormula L}, F p → T ⊢! p → ℕ ⊧ₘ p
Instances
theorem
LO.FirstOrder.Arith.SoundOn.sound
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Structure L ℕ]
{T : LO.FirstOrder.Theory L}
{F : LO.FirstOrder.SyntacticFormula L → Prop}
[self : LO.FirstOrder.Arith.SoundOn T F]
{p : LO.FirstOrder.SyntacticFormula L}
:
theorem
LO.FirstOrder.Arith.consistent_of_sound
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Structure L ℕ]
(T : LO.FirstOrder.Theory L)
(F : Set (LO.FirstOrder.SyntacticFormula L))
[LO.FirstOrder.Arith.SoundOn T F]
(hF : ⊥ ∈ F)
:
theorem
LO.FirstOrder.Arith.consequence_of
{L : LO.FirstOrder.Language}
[L.ORing]
(T : LO.FirstOrder.Theory L)
[𝐄𝐐 ≼ T]
(p : LO.FirstOrder.SyntacticFormula L)
(H : ∀ (M : Type (max u w)) [inst : LO.ORingStruc M] [inst_1 : LO.FirstOrder.Structure L M]
[inst_2 : LO.FirstOrder.Structure.ORing L M] [inst_3 : M ⊧ₘ* T], M ⊧ₘ p)
:
T ⊨ p
Equations
- LO.FirstOrder.Arith.instGoedelNumberORingOfEncodable = LO.FirstOrder.Semiterm.Operator.GoedelNumber.ofEncodable
theorem
LO.FirstOrder.Arith.goedelNumber'_def
{ξ : Type u_1}
{n : ℕ}
{α : Type u_2}
[Encodable α]
(a : α)
:
@[simp]
- refl: ∀ {L : LO.FirstOrder.Language} [inst : L.Eq], 𝐄𝐐' (“!!(LO.FirstOrder.Semiterm.fvar 0) = !!(LO.FirstOrder.Semiterm.fvar 0)”)
- replace: ∀ {L : LO.FirstOrder.Language} [inst : L.Eq] (p : LO.FirstOrder.SyntacticSemiformula L 1), 𝐄𝐐' (“∀' ∀' (!!(LO.FirstOrder.Semiterm.bvar 1) = !!(LO.FirstOrder.Semiterm.bvar 0) → !((LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 1]).hom p ➝ (LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0]).hom p))”)
Instances For
Equations
- LO.FirstOrder.Theory.«term𝐄𝐐'» = Lean.ParserDescr.node `LO.FirstOrder.Theory.term𝐄𝐐' 1024 (Lean.ParserDescr.symbol "𝐄𝐐'")
Instances For
Equations
- LO.FirstOrder.Theory.EQ'.subTheoryOfEQ = LO.System.Subtheory.ofAxm! ⋯