Documentation

Foundation.FirstOrder.Tarski.Operator

def FFL.FirstOrder.Semiterm.Operator.val {L : Language} {k : ℕ} {M : Type w} [s : Tarski.Structure L M] (v : Fin k → M) (o : Operator L k) :

M

Equations

FFL.FirstOrder.Semiterm.Operator.val v o = FFL.FirstOrder.Semiterm.val v Empty.elim o.term

Instances For

@[simp]

theorem FFL.FirstOrder.Semiterm.val_operator {L : Language} {M : Type w} {s : Tarski.Structure L M} {n : ℕ} {ξ : Type u_1} {k : ℕ} (b : Fin n → M) (f : ξ → M) (o : Operator L k) (v : Fin k → Semiterm L ξ n) :

val b f (o.operator v) = Operator.val (val b f ∘ v) o

theorem FFL.FirstOrder.Semiterm.val_operator' {L : Language} {M : Type w} {s : Tarski.Structure L M} {ξ : Type u_1} {k : ℕ} (b : Fin k → M) (f : ξ → M) (o : Operator L k) (v : Fin k → Semiterm L ξ k) :

val b f (o.operator v) = Operator.val (fun (i : Fin k) => val b f (v i)) o

theorem FFL.FirstOrder.Semiterm.Operator.val_comp {L : Language} {M : Type w} {s : Tarski.Structure L M} {k m : ℕ} (o₁ : Operator L k) (o₂ : Fin k → Operator L m) (v : Fin m → M) :

val v (o₁.comp o₂) = val (val v ∘ o₂) o₁

@[simp]

theorem FFL.FirstOrder.Semiterm.Operator.val_bvar {L : Language} {M : Type w} {s : Tarski.Structure L M} {n : ℕ} (x : Fin n) (v : Fin n → M) :

val v (bvar x) = v x

def FFL.FirstOrder.Semiformula.Operator.val {L : Language} {M : Type w} [s : Tarski.Structure L M] {k : ℕ} (v : Fin k → M) (o : Operator L k) :

Equations

FFL.FirstOrder.Semiformula.Operator.val v o = (FFL.FirstOrder.Semiformula.Eval v Empty.elim) o.sentence

Instances For

@[simp]

theorem FFL.FirstOrder.Semiformula.val_operator_and {L : Language} {M : Type w} {s : Tarski.Structure L M} {k : ℕ} {o₁ o₂ : Operator L k} {v : Fin k → M} :

Operator.val v (o₁.and o₂) ↔ Operator.val v o₁ ∧ Operator.val v o₂

@[simp]

theorem FFL.FirstOrder.Semiformula.val_operator_or {L : Language} {M : Type w} {s : Tarski.Structure L M} {k : ℕ} {o₁ o₂ : Operator L k} {v : Fin k → M} :

Operator.val v (o₁.or o₂) ↔ Operator.val v o₁ ∨ Operator.val v o₂

@[simp]

theorem FFL.FirstOrder.Semiformula.eval_operator {L : Language} {M : Type w} {s : Tarski.Structure L M} {n : ℕ} {ξ : Type u_1} {k : ℕ} {o : Operator L k} {e : Fin n → M} {f : ξ → M} {v : Fin k → Semiterm L ξ n} :

(Eval e f) (o.operator v) ↔ Operator.val (Semiterm.val e f ∘ v) o

class FFL.FirstOrder.Tarski.Structure.Zero (L : Language) (M : Type u_1) [Structure L M] [Semiterm.Operator.Zero L] [Zero M] :

zero : Semiterm.Operator.val ![] op(0) = 0

Instances

class FFL.FirstOrder.Tarski.Structure.One (L : Language) (M : Type u_1) [Structure L M] [Semiterm.Operator.One L] [One M] :

one : Semiterm.Operator.val ![] op(1) = 1

Instances

class FFL.FirstOrder.Tarski.Structure.Add (L : Language) (M : Type u_1) [Structure L M] [Semiterm.Operator.Add L] [Add M] :

add (a b : M) : Semiterm.Operator.val ![a, b] op(+) = a + b

Instances

class FFL.FirstOrder.Tarski.Structure.Mul (L : Language) (M : Type u_1) [Structure L M] [Semiterm.Operator.Mul L] [Mul M] :

mul (a b : M) : Semiterm.Operator.val ![a, b] op(*) = a * b

Instances

class FFL.FirstOrder.Tarski.Structure.Exp (L : Language) (M : Type u_1) [Structure L M] [Semiterm.Operator.Exp L] [Exp M] :

exp (a : M) : Semiterm.Operator.val ![a] Semiterm.Operator.Exp.exp = FFL.Exp.exp a

Instances

class FFL.FirstOrder.Tarski.Structure.Eq (L : Language) (M : Type u_1) [Structure L M] [Semiformula.Operator.Eq L] :

eq (a b : M) : Semiformula.Operator.val ![a, b] op(=) ↔ a = b

Instances

class FFL.FirstOrder.Tarski.Structure.LT (L : Language) (M : Type u_1) [Structure L M] [Semiformula.Operator.LT L] [LT M] :

lt (a b : M) : Semiformula.Operator.val ![a, b] op(<) ↔ a < b

Instances

class FFL.FirstOrder.Tarski.Structure.LE (L : Language) (M : Type u_1) [Structure L M] [Semiformula.Operator.LE L] [LE M] :

le (a b : M) : Semiformula.Operator.val ![a, b] op(≤) ↔ a ≤ b

Instances

class FFL.FirstOrder.Tarski.Structure.Mem (L : Language) (M : Type u_1) [Structure L M] [Semiformula.Operator.Mem L] [Membership M M] :

mem (a b : M) : Semiformula.Operator.val ![a, b] op(∈) ↔ a ∈ b

Instances

instance FFL.FirstOrder.Tarski.Structure.instLEOfEqOfLT (L : Language) (M : Type u_1) [Structure L M] [L.Eq] [L.LT] [Structure.Eq L M] [PartialOrder M] [Structure.LT L M] :

Structure.LE L M

@[simp]

theorem FFL.FirstOrder.Tarski.Structure.zero_eq_of_lang {L : Language} {M : Type u_1} [Structure L M] [L.Zero] [Zero M] [Structure.Zero L M] (v : Fin 0 → M) :

func Language.Zero.zero v = 0

@[simp]

theorem FFL.FirstOrder.Tarski.Structure.one_eq_of_lang {L : Language} {M : Type u_1} [Structure L M] [L.One] [One M] [Structure.One L M] (v : Fin 0 → M) :

func Language.One.one v = 1

@[simp]

theorem FFL.FirstOrder.Tarski.Structure.add_eq_of_lang {L : Language} {M : Type u_1} [Structure L M] [L.Add] [Add M] [Structure.Add L M] {v : Fin 2 → M} :

func Language.Add.add v = v 0 + v 1

@[simp]

theorem FFL.FirstOrder.Tarski.Structure.mul_eq_of_lang {L : Language} {M : Type u_1} [Structure L M] [L.Mul] [Mul M] [Structure.Mul L M] {v : Fin 2 → M} :

func Language.Mul.mul v = v 0 * v 1

@[simp]

theorem FFL.FirstOrder.Tarski.Structure.exp_eq_of_lang {L : Language} {M : Type u_1} [Structure L M] [L.Exp] [Exp M] [Structure.Exp L M] {v : Fin 1 → M} :

func Language.Exp.exp v = FFL.Exp.exp (v 0)

@[simp]

theorem FFL.FirstOrder.Tarski.Structure.eq_iff_eq {L : Language} {M : Type u_1} [Structure L M] [Semiformula.Operator.Eq L] [Structure.Eq L M] {v : Fin 2 → M} :

Semiformula.Operator.val v op(=) ↔ v 0 = v 1

@[simp]

theorem FFL.FirstOrder.Tarski.Structure.lt_iff_lt {L : Language} {M : Type u_1} [Structure L M] [Semiformula.Operator.LT L] [LT M] [Structure.LT L M] {v : Fin 2 → M} :

Semiformula.Operator.val v op(<) ↔ v 0 < v 1

@[simp]

theorem FFL.FirstOrder.Tarski.Structure.mem_iff_mem {L : Language} {M : Type u_1} [Structure L M] [Semiformula.Operator.Mem L] [Membership M M] [Structure.Mem L M] {v : Fin 2 → M} :

Semiformula.Operator.val v op(∈) ↔ v 0 ∈ v 1

theorem FFL.FirstOrder.Tarski.Structure.le_iff_of_eq_of_lt {L : Language} {M : Type u_1} [Structure L M] [Semiformula.Operator.Eq L] [Semiformula.Operator.LT L] [LT M] [Structure.Eq L M] [Structure.LT L M] {a b : M} :

Semiformula.Operator.val ![a, b] op(≤) ↔ a = b ∨ a < b

@[simp]

theorem FFL.FirstOrder.Tarski.Structure.eq_lang {L : Language} {M : Type u_1} [Structure L M] [L.Eq] [Structure.Eq L M] {v : Fin 2 → M} :

rel Language.Eq.eq v ↔ v 0 = v 1

@[simp]

theorem FFL.FirstOrder.Tarski.Structure.lt_lang {L : Language} {M : Type u_1} [Structure L M] [L.LT] [LT M] [Structure.LT L M] {v : Fin 2 → M} :

rel Language.LT.lt v ↔ v 0 < v 1

@[simp]

theorem FFL.FirstOrder.Tarski.Structure.mem_lang {L : Language} {M : Type u_1} [Structure L M] [L.Mem] [Membership M M] [Structure.Mem L M] {v : Fin 2 → M} :

rel Language.Mem.mem v ↔ v 0 ∈ v 1

theorem FFL.FirstOrder.Tarski.Structure.operator_val_ofEquiv_iff {L : Language} {M : Type u_1} [Structure L M] {N : Type u_2} (φ : M ≃ N) {k : ℕ} {o : Semiformula.Operator L k} {v : Fin k → N} :

Semiformula.Operator.val v o ↔ Semiformula.Operator.val (⇑φ.symm ∘ v) o

@[simp]

theorem FFL.FirstOrder.Semiformula.eval_ballLT {n : ℕ} {ξ : Type u_3} {L : Language} {M : Type u_1} {s : Tarski.Structure L M} {e : Fin n → M} {f : ξ → M} {t : Semiterm L ξ n} {φ : Semiformula L ξ (n + 1)} [Operator.LT L] [LT M] [Tarski.Structure.LT L M] :

(Eval e f) (ballLT t φ) ↔ ∀ x < Semiterm.val e f t, (Eval (x :> e) f) φ

@[simp]

theorem FFL.FirstOrder.Semiformula.eval_bexsLT {n : ℕ} {ξ : Type u_3} {L : Language} {M : Type u_1} {s : Tarski.Structure L M} {e : Fin n → M} {f : ξ → M} {t : Semiterm L ξ n} {φ : Semiformula L ξ (n + 1)} [Operator.LT L] [LT M] [Tarski.Structure.LT L M] :

(Eval e f) (bexsLT t φ) ↔ ∃ x < Semiterm.val e f t, (Eval (x :> e) f) φ

@[simp]

theorem FFL.FirstOrder.Semiformula.eval_ballLE {n : ℕ} {ξ : Type u_3} {L : Language} {M : Type u_1} {s : Tarski.Structure L M} {e : Fin n → M} {f : ξ → M} {t : Semiterm L ξ n} {φ : Semiformula L ξ (n + 1)} [Operator.LE L] [LE M] [Tarski.Structure.LE L M] :

(Eval e f) (ballLE t φ) ↔ ∀ x ≤ Semiterm.val e f t, (Eval (x :> e) f) φ

@[simp]

theorem FFL.FirstOrder.Semiformula.eval_bexsLE {n : ℕ} {ξ : Type u_3} {L : Language} {M : Type u_1} {s : Tarski.Structure L M} {e : Fin n → M} {f : ξ → M} {t : Semiterm L ξ n} {φ : Semiformula L ξ (n + 1)} [Operator.LE L] [LE M] [Tarski.Structure.LE L M] :

(Eval e f) (bexsLE t φ) ↔ ∃ x ≤ Semiterm.val e f t, (Eval (x :> e) f) φ

@[simp]

theorem FFL.FirstOrder.Semiformula.eval_ballMem {n : ℕ} {ξ : Type u_3} {L : Language} {M : Type u_1} {s : Tarski.Structure L M} {e : Fin n → M} {f : ξ → M} {t : Semiterm L ξ n} {φ : Semiformula L ξ (n + 1)} [Operator.Mem L] [Membership M M] [Tarski.Structure.Mem L M] :

(Eval e f) (ballMem t φ) ↔ ∀ x ∈ Semiterm.val e f t, (Eval (x :> e) f) φ

@[simp]

theorem FFL.FirstOrder.Semiformula.eval_bexsMem {n : ℕ} {ξ : Type u_3} {L : Language} {M : Type u_1} {s : Tarski.Structure L M} {e : Fin n → M} {f : ξ → M} {t : Semiterm L ξ n} {φ : Semiformula L ξ (n + 1)} [Operator.Mem L] [Membership M M] [Tarski.Structure.Mem L M] :

(Eval e f) (bexsMem t φ) ↔ ∃ x ∈ Semiterm.val e f t, (Eval (x :> e) f) φ