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

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Eq.refl (L : Language) [Semiformula.Operator.Eq L] : Sentence L

Equations

• LO.FirstOrder.Theory.Eq.refl L = (“∀⁰ !!(LO.FirstOrder.Semiterm.bvar 0) = !!(LO.FirstOrder.Semiterm.bvar 0)”)

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Eq.symm (L : Language) [Semiformula.Operator.Eq L] : Sentence L

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Eq.trans (L : Language) [Semiformula.Operator.Eq L] : Sentence L

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Eq.funcExt {L : Language} [Semiformula.Operator.Eq L] {k : ℕ} (f : L.Func k) : Sentence L

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Eq.relExt {L : Language} [Semiformula.Operator.Eq L] {k : ℕ} (r : L.Rel k) : Sentence L

Equations

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

inductive LO.FirstOrder.Theory.eqAxiom (L : Language) [Semiformula.Operator.Eq L] : Theory L

• refl {L : Language} [Semiformula.Operator.Eq L] : 𝗘𝗤 L (Eq.refl L)
• symm {L : Language} [Semiformula.Operator.Eq L] : 𝗘𝗤 L (Eq.symm L)
• trans {L : Language} [Semiformula.Operator.Eq L] : 𝗘𝗤 L (Eq.trans L)
• funcExt {L : Language} [Semiformula.Operator.Eq L] {k : ℕ} (f : L.Func k) : 𝗘𝗤 L (Eq.funcExt f)
• relExt {L : Language} [Semiformula.Operator.Eq L] {k : ℕ} (r : L.Rel k) : 𝗘𝗤 L (Eq.relExt r)

def LO.FirstOrder.Theory.«term𝗘𝗤» : Lean.ParserDescr

Equations

• LO.FirstOrder.Theory.«term𝗘𝗤» = Lean.ParserDescr.node `LO.FirstOrder.Theory.«term𝗘𝗤» 1024 (Lean.ParserDescr.symbol "𝗘𝗤")

theorem LO.FirstOrder.Theory.Eq.defeq {L : Language} [Semiformula.Operator.Eq L] : 𝗘𝗤 L = ({refl L, symm L, trans L} ∪ Set.range fun (f : (k : ℕ) × L.Func k) => funcExt f.snd) ∪ Set.range fun (f : (k : ℕ) × L.Rel k) => relExt f.snd

@[simp]

theorem LO.FirstOrder.Theory.EqAxiom.finite {L : Language} [Semiformula.Operator.Eq L] [L.Finite] : Set.Finite (𝗘𝗤 L)

@[simp]

instance LO.FirstOrder.Structure.Eq.models_eq (L : Language) [Semiformula.Operator.Eq L] (M : Type u_2) [Nonempty M] [Structure L M] [Structure.Eq L M] : M↓[L] ⊧* 𝗘𝗤 L

instance LO.FirstOrder.Structure.Eq.models_eqAxiom' (L : Language) [Semiformula.Operator.Eq L] (M : Type u_2) [Nonempty M] [Structure L M] [Structure.Eq L M] : M↓[L] ⊧* 𝗘𝗤 L

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

Equations

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

theorem LO.FirstOrder.Structure.Eq.eqv_refl {L : Language} [Semiformula.Operator.Eq L] {M : Type u_2} [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] (a : M) : eqv L a a

theorem LO.FirstOrder.Structure.Eq.eqv_symm {L : Language} [Semiformula.Operator.Eq L] {M : Type u_2} [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] {a b : M} : eqv L a b → eqv L b a

theorem LO.FirstOrder.Structure.Eq.eqv_trans {L : Language} [Semiformula.Operator.Eq L] {M : Type u_2} [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] {a b c : M} : eqv L a b → eqv L b c → eqv L a c

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

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

theorem LO.FirstOrder.Structure.Eq.eqv_relExt {L : Language} [Semiformula.Operator.Eq L] {M : Type u_2} [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] {k : ℕ} (r : L.Rel k) {v w : Fin k → M} (h : ∀ (i : Fin k), eqv L (v i) (w i)) : rel r v ↔ rel r w

theorem LO.FirstOrder.Structure.Eq.eqv_equivalence {L : Language} [Semiformula.Operator.Eq L] {M : Type u_2} [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] : Equivalence (eqv L)

def LO.FirstOrder.Structure.Eq.eqvSetoid (L : Language) [Semiformula.Operator.Eq L] (M : Type u_2) [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] : Setoid M

Equations

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

def LO.FirstOrder.Structure.Eq.QuotEq (L : Language) [Semiformula.Operator.Eq L] (M : Type u_2) [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] : Type u_2

Equations

• LO.FirstOrder.Structure.Eq.QuotEq L M = Quotient (LO.FirstOrder.Structure.Eq.eqvSetoid L M)

instance LO.FirstOrder.Structure.Eq.QuotEq.inhabited {L : Language} [Semiformula.Operator.Eq L] {M : Type u_2} [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] : Nonempty (QuotEq L M)

theorem LO.FirstOrder.Structure.Eq.of_eq_of {L : Language} [Semiformula.Operator.Eq L] {M : Type u_2} [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] {a b : M} : ⟦a⟧ = ⟦b⟧ ↔ eqv L a b

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

Equations

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

def LO.FirstOrder.Structure.Eq.QuotEq.Rel {L : Language} [Semiformula.Operator.Eq L] {M : Type u_2} [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] ⦃k : ℕ⦄ (r : L.Rel k) (v : Fin k → QuotEq L M) : Prop

Equations

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

@[implicit_reducible]

instance LO.FirstOrder.Structure.Eq.QuotEq.struc {L : Language} [Semiformula.Operator.Eq L] {M : Type u_2} [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] : Structure L (QuotEq L M)

Equations

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

theorem LO.FirstOrder.Structure.Eq.QuotEq.funk_mk {L : Language} [Semiformula.Operator.Eq L] {M : Type u_2} [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] {k : ℕ} (f : L.Func k) (v : Fin k → M) : (Structure.func f fun (x : Fin k) => ⟦v x⟧) = ⟦Structure.func f v⟧

theorem LO.FirstOrder.Structure.Eq.QuotEq.rel_mk {L : Language} [Semiformula.Operator.Eq L] {M : Type u_2} [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] {k : ℕ} (r : L.Rel k) (v : Fin k → M) : (rel r fun (x : Fin k) => ⟦v x⟧) ↔ rel r v

theorem LO.FirstOrder.Structure.Eq.QuotEq.val_mk {L : Language} {ξ : Type u_1} [Semiformula.Operator.Eq L] {M : Type u_2} [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] {n : ℕ} {bv : Fin n → M} {fv : ξ → M} (t : Semiterm L ξ n) : Semiterm.val (fun (x : Fin n) => ⟦bv x⟧) (fun (x : ξ) => ⟦fv x⟧) t = ⟦Semiterm.val bv fv t⟧

theorem LO.FirstOrder.Structure.Eq.QuotEq.eval_mk {L : Language} {ξ : Type u_1} [Semiformula.Operator.Eq L] {M : Type u_2} [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] {n : ℕ} {bv : Fin n → M} {fv : ξ → M} {φ : Semiformula L ξ n} : (Semiformula.Eval (fun (x : Fin n) => ⟦bv x⟧) fun (x : ξ) => ⟦fv x⟧) φ ↔ (Semiformula.Eval bv fv) φ

theorem LO.FirstOrder.Structure.Eq.QuotEq.evalf_mk {L : Language} {ξ : Type u_1} [Semiformula.Operator.Eq L] {M : Type u_2} [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] {fv : ξ → M} {φ : Formula L ξ} : (Semiformula.Evalf fun (x : ξ) => ⟦fv x⟧) φ ↔ (Semiformula.Evalf fv) φ

theorem LO.FirstOrder.Structure.Eq.QuotEq.models_iff {L : Language} [Semiformula.Operator.Eq L] {M : Type u_2} [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] {σ : Sentence L} : (QuotEq L M)↓[L] ⊧ σ ↔ M↓[L] ⊧ σ

theorem LO.FirstOrder.Structure.Eq.QuotEq.elementaryEquiv (L : Language) [Semiformula.Operator.Eq L] (M : Type u_2) [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] : QuotEq L M ≡ₑ[L] M

theorem LO.FirstOrder.Structure.Eq.QuotEq.rel_eq {L : Language} [Semiformula.Operator.Eq L] {M : Type u_2} [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] (a b : QuotEq L M) : Semiformula.Operator.val ![a, b] op(=) ↔ a = b

instance LO.FirstOrder.Structure.Eq.QuotEq.structureEq {L : Language} [Semiformula.Operator.Eq L] {M : Type u_2} [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] : Structure.Eq L (QuotEq L M)

theorem LO.FirstOrder.consequence_iff_eq {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝗘𝗤 L ⪯ T] {σ : Sentence L} : T ⊨[Struc L] σ ↔ ∀ (M : Type v) [inst : Nonempty M] [inst_1 : Structure L M] [Structure.Eq L M], M↓[L] ⊧* T → M↓[L] ⊧ σ

theorem LO.FirstOrder.consequence_iff_eq' {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝗘𝗤 L ⪯ T] {σ : Sentence L} : T ⊨[Struc L] σ ↔ ∀ (M : Type v) [inst : Nonempty M] [inst_1 : Structure L M] [Structure.Eq L M] [M↓[L] ⊧* T], M↓[L] ⊧ σ

theorem LO.FirstOrder.satisfiable_iff_eq {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝗘𝗤 L ⪯ T] : Semantics.Satisfiable (Struc L) T ↔ ∃ (M : Type v) (x : Nonempty M) (x_1 : Structure L M) (_ : Structure.Eq L M), M↓[L] ⊧* T

instance LO.FirstOrder.instModelsSetStrucSentenceStrModelOfSatEqAxiomOfWeakerThanTheory {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝗘𝗤 L ⪯ T] (sat : Semantics.Satisfiable (Struc L) T) : (ModelOfSat sat)↓[L] ⊧* 𝗘𝗤 L

def LO.FirstOrder.ModelOfSatEq {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝗘𝗤 L ⪯ T] (sat : Semantics.Satisfiable (Struc L) T) : Type v

Equations

• LO.FirstOrder.ModelOfSatEq sat = LO.FirstOrder.Structure.Eq.QuotEq L (LO.FirstOrder.ModelOfSat sat)

instance LO.FirstOrder.ModelOfSatEq.instNonempty {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝗘𝗤 L ⪯ T] (sat : Semantics.Satisfiable (Struc L) T) : Nonempty (ModelOfSatEq sat)

@[implicit_reducible]

noncomputable instance LO.FirstOrder.ModelOfSatEq.struc {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝗘𝗤 L ⪯ T] (sat : Semantics.Satisfiable (Struc L) T) : Structure L (ModelOfSatEq sat)

Equations

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

instance LO.FirstOrder.ModelOfSatEq.instEq {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝗘𝗤 L ⪯ T] (sat : Semantics.Satisfiable (Struc L) T) : Structure.Eq L (ModelOfSatEq sat)

theorem LO.FirstOrder.ModelOfSatEq.models {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝗘𝗤 L ⪯ T] (sat : Semantics.Satisfiable (Struc L) T) : (ModelOfSatEq sat)↓[L] ⊧* T

instance LO.FirstOrder.ModelOfSatEq.mod {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝗘𝗤 L ⪯ T] (sat : Semantics.Satisfiable (Struc L) T) : (ModelOfSatEq sat)↓[L] ⊧* T

@[implicit_reducible]

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

Equations

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

instance LO.FirstOrder.ModelOfSatEq.strucZero {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝗘𝗤 L ⪯ T] (sat : Semantics.Satisfiable (Struc L) T) [Semiterm.Operator.Zero L] : Structure.Zero L (ModelOfSatEq sat)

@[implicit_reducible]

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

Equations

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

instance LO.FirstOrder.ModelOfSatEq.instOne {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝗘𝗤 L ⪯ T] (sat : Semantics.Satisfiable (Struc L) T) [Semiterm.Operator.One L] : Structure.One L (ModelOfSatEq sat)

@[implicit_reducible]

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

Equations

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

instance LO.FirstOrder.ModelOfSatEq.instAdd {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝗘𝗤 L ⪯ T] (sat : Semantics.Satisfiable (Struc L) T) [Semiterm.Operator.Add L] : Structure.Add L (ModelOfSatEq sat)

@[implicit_reducible]

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

Equations

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

instance LO.FirstOrder.ModelOfSatEq.instMul {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝗘𝗤 L ⪯ T] (sat : Semantics.Satisfiable (Struc L) T) [Semiterm.Operator.Mul L] : Structure.Mul L (ModelOfSatEq sat)

@[implicit_reducible]

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

Equations

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

instance LO.FirstOrder.ModelOfSatEq.instLT {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝗘𝗤 L ⪯ T] (sat : Semantics.Satisfiable (Struc L) T) [Semiformula.Operator.LT L] : Structure.LT L (ModelOfSatEq sat)

@[implicit_reducible]

instance LO.FirstOrder.ModelOfSatEq.instMembershipOfMem {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝗘𝗤 L ⪯ T] (sat : Semantics.Satisfiable (Struc L) T) [Semiformula.Operator.Mem L] : Membership (ModelOfSatEq sat) (ModelOfSatEq sat)

Equations

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

instance LO.FirstOrder.ModelOfSatEq.instMem {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝗘𝗤 L ⪯ T] (sat : Semantics.Satisfiable (Struc L) T) [Semiformula.Operator.Mem L] : Structure.Mem L (ModelOfSatEq sat)

def LO.FirstOrder.Semiformula.existsUnique {L : Language} [Operator.Eq L] {n : ℕ} {ξ : Type u_3} (φ : Semiformula L ξ (n + 1)) : Semiformula L ξ n

Equations

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

def LO.FirstOrder.Semiformula.«term∃⁰!_» : Lean.ParserDescr

Equations

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

@[simp]

theorem LO.FirstOrder.Semiformula.eval_existsUnique {L : Language} {ξ : Type u_1} [Operator.Eq L] {M : Type u_2} [s : Structure L M] [Structure.Eq L M] {n : ℕ} {e : Fin n → M} {ε : ξ → M} {φ : Semiformula L ξ (n + 1)} : (Eval e ε) (∃⁰! φ) ↔ ∃! x : M, (Eval (x :> e) ε) φ

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

Equations

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

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

Equations

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