Logic.FirstOrder.Basic.Eq

source

def Matrix.iget {α : Type u_1} {k : ℕ} [Inhabited α] (v : Fin k → α) (x : ℕ) :

Equations

Matrix.iget v x = if h : x < k then v ⟨x, h⟩ else default

source

class LO.FirstOrder.Theory.Sub {L : LO.FirstOrder.Language} (T : LO.FirstOrder.Theory L) (U : LO.FirstOrder.Theory L) :

Type

sub : T ⊆ U

Instances

source

theorem LO.FirstOrder.Theory.Sub.sub {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {U : LO.FirstOrder.Theory L} [self : T.Sub U] :

T ⊆ U

source

inductive LO.FirstOrder.Theory.eqAxiom {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] :

LO.FirstOrder.Theory L

refl: ∀ {L : LO.FirstOrder.Language} [inst : LO.FirstOrder.Semiformula.Operator.Eq L], 𝐄𝐐 (“!!(LO.FirstOrder.Semiterm.fvar 0) = !!(LO.FirstOrder.Semiterm.fvar 0)”)
symm: ∀ {L : LO.FirstOrder.Language} [inst : LO.FirstOrder.Semiformula.Operator.Eq L], 𝐄𝐐 (“(!!(LO.FirstOrder.Semiterm.fvar 0) = !!(LO.FirstOrder.Semiterm.fvar 1) → !!(LO.FirstOrder.Semiterm.fvar 1) = !!(LO.FirstOrder.Semiterm.fvar 0))”)
trans: ∀ {L : LO.FirstOrder.Language} [inst : LO.FirstOrder.Semiformula.Operator.Eq L], 𝐄𝐐 (“(!!(LO.FirstOrder.Semiterm.fvar 0) = !!(LO.FirstOrder.Semiterm.fvar 1) → (!!(LO.FirstOrder.Semiterm.fvar 1) = !!(LO.FirstOrder.Semiterm.fvar 2) → !!(LO.FirstOrder.Semiterm.fvar 0) = !!(LO.FirstOrder.Semiterm.fvar 2)))”)
funcExt: ∀ {L : LO.FirstOrder.Language} [inst : LO.FirstOrder.Semiformula.Operator.Eq L] {k : ℕ} (f : L.Func k), 𝐄𝐐 (“(!(Matrix.conj fun (i : Fin k) => “!!(LO.FirstOrder.Semiterm.fvar ↑i) = !!(LO.FirstOrder.Semiterm.fvar (k + ↑i))”) → !!(LO.FirstOrder.Semiterm.func f fun (i : Fin k) => LO.FirstOrder.Semiterm.fvar ↑i) = !!(LO.FirstOrder.Semiterm.func f fun (i : Fin k) => LO.FirstOrder.Semiterm.fvar (k + ↑i)))”)
relExt: ∀ {L : LO.FirstOrder.Language} [inst : LO.FirstOrder.Semiformula.Operator.Eq L] {k : ℕ} (r : L.Rel k), 𝐄𝐐 ((Matrix.conj fun (i : Fin k) => “!!(LO.FirstOrder.Semiterm.fvar ↑i) = !!(LO.FirstOrder.Semiterm.fvar (k + ↑i))”) ➝ (LO.FirstOrder.Semiformula.rel r fun (i : Fin k) => LO.FirstOrder.Semiterm.fvar ↑i) ➝ LO.FirstOrder.Semiformula.rel r fun (i : Fin k) => LO.FirstOrder.Semiterm.fvar (k + ↑i))

Instances For

source

def LO.FirstOrder.Theory.«term𝐄𝐐» :

Lean.ParserDescr

Equations

LO.FirstOrder.Theory.«term𝐄𝐐» = Lean.ParserDescr.node `LO.FirstOrder.Theory.term𝐄𝐐 1024 (Lean.ParserDescr.symbol "𝐄𝐐")

source

@[simp]

theorem LO.FirstOrder.Structure.Eq.models_eqAxiom {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] [LO.FirstOrder.Structure.Eq L M] :

M ⊧ₘ* 𝐄𝐐

source

instance LO.FirstOrder.Structure.Eq.models_eqAxiom' (L : LO.FirstOrder.Language) [LO.FirstOrder.Semiformula.Operator.Eq L] (M : Type u) [Nonempty M] [LO.FirstOrder.Structure L M] [LO.FirstOrder.Structure.Eq L M] :

M ⊧ₘ* 𝐄𝐐

Equations

⋯ = ⋯

source

def LO.FirstOrder.Structure.Eq.eqv (L : LO.FirstOrder.Language) [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [LO.FirstOrder.Structure L M] (a : M) (b : M) :

Prop

Equations

LO.FirstOrder.Structure.Eq.eqv L a b = op(=).val ![a, b]

source

theorem LO.FirstOrder.Structure.Eq.eqv_refl {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] (H : M ⊧ₘ* 𝐄𝐐) (a : M) :

LO.FirstOrder.Structure.Eq.eqv L a a

source

theorem LO.FirstOrder.Structure.Eq.eqv_symm {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] (H : M ⊧ₘ* 𝐄𝐐) {a : M} {b : M} :

LO.FirstOrder.Structure.Eq.eqv L a b → LO.FirstOrder.Structure.Eq.eqv L b a

source

theorem LO.FirstOrder.Structure.Eq.eqv_trans {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] (H : M ⊧ₘ* 𝐄𝐐) {a : M} {b : M} {c : M} :

LO.FirstOrder.Structure.Eq.eqv L a b → LO.FirstOrder.Structure.Eq.eqv L b c → LO.FirstOrder.Structure.Eq.eqv L a c

source

theorem LO.FirstOrder.Structure.Eq.eqv_funcExt {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] (H : M ⊧ₘ* 𝐄𝐐) {k : ℕ} (f : L.Func k) {v : Fin k → M} {w : Fin k → M} (h : ∀ (i : Fin k), LO.FirstOrder.Structure.Eq.eqv L (v i) (w i)) :

LO.FirstOrder.Structure.Eq.eqv L (LO.FirstOrder.Structure.func f v) (LO.FirstOrder.Structure.func f w)

source

theorem LO.FirstOrder.Structure.Eq.eqv_relExt_aux {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] (H : M ⊧ₘ* 𝐄𝐐) {k : ℕ} (r : L.Rel k) {v : Fin k → M} {w : Fin k → M} (h : ∀ (i : Fin k), LO.FirstOrder.Structure.Eq.eqv L (v i) (w i)) :

LO.FirstOrder.Structure.rel r v → LO.FirstOrder.Structure.rel r w

source

theorem LO.FirstOrder.Structure.Eq.eqv_relExt {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] (H : M ⊧ₘ* 𝐄𝐐) {k : ℕ} (r : L.Rel k) {v : Fin k → M} {w : Fin k → M} (h : ∀ (i : Fin k), LO.FirstOrder.Structure.Eq.eqv L (v i) (w i)) :

LO.FirstOrder.Structure.rel r v = LO.FirstOrder.Structure.rel r w

source

theorem LO.FirstOrder.Structure.Eq.eqv_equivalence {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] (H : M ⊧ₘ* 𝐄𝐐) :

Equivalence (LO.FirstOrder.Structure.Eq.eqv L)

source

def LO.FirstOrder.Structure.Eq.eqvSetoid {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] (H : M ⊧ₘ* 𝐄𝐐) :

Setoid M

Equations

LO.FirstOrder.Structure.Eq.eqvSetoid H = { r := LO.FirstOrder.Structure.Eq.eqv L, iseqv := ⋯ }

source

def LO.FirstOrder.Structure.Eq.QuotEq {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] (H : M ⊧ₘ* 𝐄𝐐) :

Type u

Equations

LO.FirstOrder.Structure.Eq.QuotEq H = Quotient (LO.FirstOrder.Structure.Eq.eqvSetoid H)

Instances For

source

instance LO.FirstOrder.Structure.Eq.QuotEq.inhabited {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] (H : M ⊧ₘ* 𝐄𝐐) :

Nonempty (LO.FirstOrder.Structure.Eq.QuotEq H)

Equations

⋯ = ⋯

source

theorem LO.FirstOrder.Structure.Eq.of_eq_of {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] (H : M ⊧ₘ* 𝐄𝐐) {a : M} {b : M} :

⟦a⟧ = ⟦b⟧ ↔ LO.FirstOrder.Structure.Eq.eqv L a b

source

def LO.FirstOrder.Structure.Eq.QuotEq.func {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] (H : M ⊧ₘ* 𝐄𝐐) ⦃k : ℕ⦄ (f : L.Func k) (v : Fin k → LO.FirstOrder.Structure.Eq.QuotEq H) :

LO.FirstOrder.Structure.Eq.QuotEq H

Equations

LO.FirstOrder.Structure.Eq.QuotEq.func H f v = Quotient.liftVec (fun (x : Fin k → M) => ⟦LO.FirstOrder.Structure.func f x⟧) ⋯ v

source

def LO.FirstOrder.Structure.Eq.QuotEq.rel {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] (H : M ⊧ₘ* 𝐄𝐐) ⦃k : ℕ⦄ (r : L.Rel k) (v : Fin k → LO.FirstOrder.Structure.Eq.QuotEq H) :

Prop

Equations

LO.FirstOrder.Structure.Eq.QuotEq.rel H r v = Quotient.liftVec (LO.FirstOrder.Structure.rel r) ⋯ v

source

instance LO.FirstOrder.Structure.Eq.QuotEq.struc {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] {H : M ⊧ₘ* 𝐄𝐐} :

LO.FirstOrder.Structure L (LO.FirstOrder.Structure.Eq.QuotEq H)

Equations

LO.FirstOrder.Structure.Eq.QuotEq.struc = { func := LO.FirstOrder.Structure.Eq.QuotEq.func H, rel := LO.FirstOrder.Structure.Eq.QuotEq.rel H }

source

theorem LO.FirstOrder.Structure.Eq.QuotEq.funk_mk {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] {H : M ⊧ₘ* 𝐄𝐐} {k : ℕ} (f : L.Func k) (v : Fin k → M) :

(LO.FirstOrder.Structure.func f fun (i : Fin k) => ⟦v i⟧) = ⟦LO.FirstOrder.Structure.func f v⟧

source

theorem LO.FirstOrder.Structure.Eq.QuotEq.rel_mk {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] {H : M ⊧ₘ* 𝐄𝐐} {k : ℕ} (r : L.Rel k) (v : Fin k → M) :

(LO.FirstOrder.Structure.rel r fun (i : Fin k) => ⟦v i⟧) ↔ LO.FirstOrder.Structure.rel r v

source

theorem LO.FirstOrder.Structure.Eq.QuotEq.val_mk {L : LO.FirstOrder.Language} {μ : Type u_1} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] {H : M ⊧ₘ* 𝐄𝐐} {n : ℕ} {e : Fin n → M} {ε : μ → M} (t : LO.FirstOrder.Semiterm L μ n) :

LO.FirstOrder.Semiterm.valm (LO.FirstOrder.Structure.Eq.QuotEq H) (fun (i : Fin n) => ⟦e i⟧) (fun (i : μ) => ⟦ε i⟧) t = ⟦LO.FirstOrder.Semiterm.valm M e ε t⟧

source

theorem LO.FirstOrder.Structure.Eq.QuotEq.eval_mk {L : LO.FirstOrder.Language} {μ : Type u_1} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] {H : M ⊧ₘ* 𝐄𝐐} {n : ℕ} {e : Fin n → M} {ε : μ → M} {p : LO.FirstOrder.Semiformula L μ n} :

(LO.FirstOrder.Semiformula.Evalm (LO.FirstOrder.Structure.Eq.QuotEq H) (fun (i : Fin n) => ⟦e i⟧) fun (i : μ) => ⟦ε i⟧) p ↔ (LO.FirstOrder.Semiformula.Evalm M e ε) p

source

theorem LO.FirstOrder.Structure.Eq.QuotEq.eval_mk₀ {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] {H : M ⊧ₘ* 𝐄𝐐} {ξ : Type u_2} {ε : ξ → M} {p : LO.FirstOrder.Formula L ξ} :

(LO.FirstOrder.Semiformula.Evalfm (LO.FirstOrder.Structure.Eq.QuotEq H) fun (i : ξ) => ⟦ε i⟧) p ↔ (LO.FirstOrder.Semiformula.Evalfm M ε) p

source

theorem LO.FirstOrder.Structure.Eq.QuotEq.models_iff {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] {H : M ⊧ₘ* 𝐄𝐐} {p : LO.FirstOrder.SyntacticFormula L} :

LO.FirstOrder.Structure.Eq.QuotEq H ⊧ₘ p ↔ M ⊧ₘ p

source

theorem LO.FirstOrder.Structure.Eq.QuotEq.elementaryEquiv {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] (H : M ⊧ₘ* 𝐄𝐐) :

LO.FirstOrder.Structure.Eq.QuotEq H ≡ₑ[L] M

source

theorem LO.FirstOrder.Structure.Eq.QuotEq.rel_eq {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] {H : M ⊧ₘ* 𝐄𝐐} (a : LO.FirstOrder.Structure.Eq.QuotEq H) (b : LO.FirstOrder.Structure.Eq.QuotEq H) :

op(=).val ![a, b] ↔ a = b

source

instance LO.FirstOrder.Structure.Eq.QuotEq.structureEq {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] {H : M ⊧ₘ* 𝐄𝐐} :

LO.FirstOrder.Structure.Eq L (LO.FirstOrder.Structure.Eq.QuotEq H)

Equations

⋯ = ⋯

source

theorem LO.FirstOrder.consequence_iff_eq {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] {p : LO.FirstOrder.SyntacticFormula L} :

T ⊨[LO.FirstOrder.Struc L] p ↔ ∀ (M : Type v) [inst : Nonempty M] [inst_1 : LO.FirstOrder.Structure L M] [inst_2 : LO.FirstOrder.Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ p

source

theorem LO.FirstOrder.consequence_iff_eq' {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] {p : LO.FirstOrder.SyntacticFormula L} :

T ⊨[LO.FirstOrder.Struc L] p ↔ ∀ (M : Type v) [inst : Nonempty M] [inst_1 : LO.FirstOrder.Structure L M] [inst_2 : LO.FirstOrder.Structure.Eq L M] [inst_3 : M ⊧ₘ* T], M ⊧ₘ p

source

theorem LO.FirstOrder.satisfiable_iff_eq {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] :

LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T ↔ ∃ (M : Type v) (x : Nonempty M) (x_1 : LO.FirstOrder.Structure L M) (_ : LO.FirstOrder.Structure.Eq L M), M ⊧ₘ* T

source

def LO.FirstOrder.ModelOfSatEq {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] (sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) :

Type v

Equations

LO.FirstOrder.ModelOfSatEq sat = let_fun H := ⋯; LO.FirstOrder.Structure.Eq.QuotEq H

Instances For

source

noncomputable instance LO.FirstOrder.ModelOfSatEq.instNonempty {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] (sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) :

Nonempty (LO.FirstOrder.ModelOfSatEq sat)

Equations

⋯ = ⋯

source

noncomputable instance LO.FirstOrder.ModelOfSatEq.struc {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] (sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) :

LO.FirstOrder.Structure L (LO.FirstOrder.ModelOfSatEq sat)

Equations

LO.FirstOrder.ModelOfSatEq.struc sat = LO.FirstOrder.Structure.Eq.QuotEq.struc

source

noncomputable instance LO.FirstOrder.ModelOfSatEq.instEq {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] (sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) :

LO.FirstOrder.Structure.Eq L (LO.FirstOrder.ModelOfSatEq sat)

Equations

⋯ = ⋯

source

theorem LO.FirstOrder.ModelOfSatEq.models {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] (sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) :

LO.FirstOrder.ModelOfSatEq sat ⊧ₘ* T

source

instance LO.FirstOrder.ModelOfSatEq.mod {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] (sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) :

LO.FirstOrder.ModelOfSatEq sat ⊧ₘ* T

Equations

⋯ = ⋯

source

noncomputable instance LO.FirstOrder.ModelOfSatEq.instZeroOfZero {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] (sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) [LO.FirstOrder.Semiterm.Operator.Zero L] :

Zero (LO.FirstOrder.ModelOfSatEq sat)

Equations

LO.FirstOrder.ModelOfSatEq.instZeroOfZero sat = { zero := LO.FirstOrder.Semiterm.Operator.val op(0) ![] }

source

instance LO.FirstOrder.ModelOfSatEq.strucZero {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] (sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) [LO.FirstOrder.Semiterm.Operator.Zero L] :

LO.FirstOrder.Structure.Zero L (LO.FirstOrder.ModelOfSatEq sat)

Equations

⋯ = ⋯

source

noncomputable instance LO.FirstOrder.ModelOfSatEq.instOneOfOne {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] (sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) [LO.FirstOrder.Semiterm.Operator.One L] :

One (LO.FirstOrder.ModelOfSatEq sat)

Equations

LO.FirstOrder.ModelOfSatEq.instOneOfOne sat = { one := LO.FirstOrder.Semiterm.Operator.val op(1) ![] }

source

instance LO.FirstOrder.ModelOfSatEq.instOne {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] (sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) [LO.FirstOrder.Semiterm.Operator.One L] :

LO.FirstOrder.Structure.One L (LO.FirstOrder.ModelOfSatEq sat)

Equations

⋯ = ⋯

source

noncomputable instance LO.FirstOrder.ModelOfSatEq.instAddOfAdd {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] (sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) [LO.FirstOrder.Semiterm.Operator.Add L] :

Add (LO.FirstOrder.ModelOfSatEq sat)

Equations

LO.FirstOrder.ModelOfSatEq.instAddOfAdd sat = { add := fun (x y : LO.FirstOrder.ModelOfSatEq sat) => op(+).val ![x, y] }

source

instance LO.FirstOrder.ModelOfSatEq.instAdd {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] (sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) [LO.FirstOrder.Semiterm.Operator.Add L] :

LO.FirstOrder.Structure.Add L (LO.FirstOrder.ModelOfSatEq sat)

Equations

⋯ = ⋯

source

noncomputable instance LO.FirstOrder.ModelOfSatEq.instMulOfMul {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] (sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) [LO.FirstOrder.Semiterm.Operator.Mul L] :

Mul (LO.FirstOrder.ModelOfSatEq sat)

Equations

LO.FirstOrder.ModelOfSatEq.instMulOfMul sat = { mul := fun (x y : LO.FirstOrder.ModelOfSatEq sat) => op(*).val ![x, y] }

source

instance LO.FirstOrder.ModelOfSatEq.instMul {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] (sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) [LO.FirstOrder.Semiterm.Operator.Mul L] :

LO.FirstOrder.Structure.Mul L (LO.FirstOrder.ModelOfSatEq sat)

Equations

⋯ = ⋯

source

instance LO.FirstOrder.ModelOfSatEq.instLTOfLT {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] (sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) [LO.FirstOrder.Semiformula.Operator.LT L] :

LT (LO.FirstOrder.ModelOfSatEq sat)

Equations

LO.FirstOrder.ModelOfSatEq.instLTOfLT sat = { lt := fun (x y : LO.FirstOrder.ModelOfSatEq sat) => op(<).val ![x, y] }

source

instance LO.FirstOrder.ModelOfSatEq.instLT {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] (sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) [LO.FirstOrder.Semiformula.Operator.LT L] :

LO.FirstOrder.Structure.LT L (LO.FirstOrder.ModelOfSatEq sat)

Equations

⋯ = ⋯

source

instance LO.FirstOrder.ModelOfSatEq.instMembershipOfMem {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] (sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) [LO.FirstOrder.Semiformula.Operator.Mem L] :

Membership (LO.FirstOrder.ModelOfSatEq sat) (LO.FirstOrder.ModelOfSatEq sat)

Equations

LO.FirstOrder.ModelOfSatEq.instMembershipOfMem sat = { mem := fun (x y : LO.FirstOrder.ModelOfSatEq sat) => op(∈).val ![x, y] }

source

instance LO.FirstOrder.ModelOfSatEq.instMem {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] (sat : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) [LO.FirstOrder.Semiformula.Operator.Mem L] :

LO.FirstOrder.Structure.Mem L (LO.FirstOrder.ModelOfSatEq sat)

Equations

⋯ = ⋯

source

def LO.FirstOrder.Semiformula.existsUnique {L : LO.FirstOrder.Language} {μ : Type u_1} [LO.FirstOrder.Semiformula.Operator.Eq L] {n : ℕ} (p : LO.FirstOrder.Semiformula L μ (n + 1)) :

LO.FirstOrder.Semiformula L μ n

Equations

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

source

def LO.FirstOrder.Semiformula.«term∃'!_» :

Lean.ParserDescr

Equations

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

source

@[simp]

theorem LO.FirstOrder.Semiformula.eval_existsUnique {L : LO.FirstOrder.Language} {μ : Type u_1} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u_2} [s : LO.FirstOrder.Structure L M] [LO.FirstOrder.Structure.Eq L M] {n : ℕ} {e : Fin n → M} {ε : μ → M} {p : LO.FirstOrder.Semiformula L μ (n + 1)} :

(LO.FirstOrder.Semiformula.Eval s e ε) (∃'! p) ↔ ∃! x : M, (LO.FirstOrder.Semiformula.Eval s (x :> e) ε) p

source

def LO.FirstOrder.BinderNotation.«first_order_formula∃!_» :

Lean.ParserDescr

Equations

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

source

def LO.FirstOrder.BinderNotation.«first_order_formula∃!_,_» :

Lean.ParserDescr

Equations

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