Foundation.FirstOrder.Tarski.Eq

@[simp]

instance FFL.FirstOrder.Tarski.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

source

instance FFL.FirstOrder.Tarski.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

source

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

Prop

Equations

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

Instances For

source

theorem FFL.FirstOrder.Tarski.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

source

theorem FFL.FirstOrder.Tarski.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

source

theorem FFL.FirstOrder.Tarski.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

source

theorem FFL.FirstOrder.Tarski.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)

source

theorem FFL.FirstOrder.Tarski.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

source

theorem FFL.FirstOrder.Tarski.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

source

theorem FFL.FirstOrder.Tarski.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)

source

def FFL.FirstOrder.Tarski.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

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

Instances For

source

def FFL.FirstOrder.Tarski.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

FFL.FirstOrder.Tarski.Structure.Eq.QuotEq L M = Quotient (FFL.FirstOrder.Tarski.Structure.Eq.eqvSetoid L M)

Instances For

source

instance FFL.FirstOrder.Tarski.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)

source

theorem FFL.FirstOrder.Tarski.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

source

def FFL.FirstOrder.Tarski.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

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

Instances For

source

def FFL.FirstOrder.Tarski.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

FFL.FirstOrder.Tarski.Structure.Eq.QuotEq.Rel r v = Quotient.liftVec (FFL.FirstOrder.Tarski.Structure.rel r) ⋯ v

Instances For

source

@[instance_reducible]

instance FFL.FirstOrder.Tarski.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

FFL.FirstOrder.Tarski.Structure.Eq.QuotEq.struc = { func := FFL.FirstOrder.Tarski.Structure.Eq.QuotEq.func, rel := FFL.FirstOrder.Tarski.Structure.Eq.QuotEq.Rel }

source

theorem FFL.FirstOrder.Tarski.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⟧

source

theorem FFL.FirstOrder.Tarski.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

source

theorem FFL.FirstOrder.Tarski.Structure.Eq.QuotEq.funk_mk_of_eq {L : Language} [Semiformula.Operator.Eq L] {M : Type u_2} [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] {k : ℕ} (f : L.Func k) {w : Fin k → QuotEq L M} {v : Fin k → M} (h : ∀ (i : Fin k), w i = ⟦v i⟧) :

Structure.func f w = ⟦Structure.func f v⟧

source

theorem FFL.FirstOrder.Tarski.Structure.Eq.QuotEq.rel_mk_of_eq {L : Language} [Semiformula.Operator.Eq L] {M : Type u_2} [Nonempty M] [Structure L M] [H : M↓[L] ⊧* 𝗘𝗤 L] {k : ℕ} (r : L.Rel k) {w : Fin k → QuotEq L M} {v : Fin k → M} (h : ∀ (i : Fin k), w i = ⟦v i⟧) :

rel r w ↔ rel r v

source

theorem FFL.FirstOrder.Tarski.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⟧

source

theorem FFL.FirstOrder.Tarski.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) φ

source

theorem FFL.FirstOrder.Tarski.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) φ

source

theorem FFL.FirstOrder.Tarski.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] ⊧ σ

source

theorem FFL.FirstOrder.Tarski.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

source

theorem FFL.FirstOrder.Tarski.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

source

instance FFL.FirstOrder.Tarski.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)

source

theorem FFL.FirstOrder.consequence_iff_eq_of_models_eq {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} (hEq : ∀ (M : Type v) [inst : Nonempty M] [inst_1 : Tarski.Structure L M], M↓[L] ⊧* T → M↓[L] ⊧* 𝗘𝗤 L) {σ : Sentence L} :

T ⊨[Tarski.Struc L] σ ↔ ∀ (M : Type v) [inst : Nonempty M] [inst_1 : Tarski.Structure L M] [Tarski.Structure.Eq L M], M↓[L] ⊧* T → M↓[L] ⊧ σ

Consequence can be tested on equality structures when all models satisfy the equality axioms. This is a routine consequence of the quotient-model construction.

source

theorem FFL.FirstOrder.satisfiable_iff_eq_of_models_eq {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} (hEq : ∀ (M : Type v) [inst : Nonempty M] [inst_1 : Tarski.Structure L M], M↓[L] ⊧* T → M↓[L] ⊧* 𝗘𝗤 L) :

Semantics.Satisfiable (Tarski.Struc L) T ↔ ∃ (M : Type v) (x : Nonempty M) (x_1 : Tarski.Structure L M) (_ : Tarski.Structure.Eq L M), M↓[L] ⊧* T

Satisfiability has an equality-structure witness when all models satisfy the equality axioms. This is a routine consequence of the quotient-model construction.

source

@[simp]

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

(Eval e ε) (∃¹! φ) ↔ ∃! x : M, (Eval (x :> e) ε) φ