def LO.Propositional.Classical.Formula.valAux {α : Type u_1} {F : Type u_2} [LO.LogicalConnective F] (v : α → F) : LO.Propositional.Classical.Formula α → F

Equations

• LO.Propositional.Classical.Formula.valAux v (LO.Propositional.Classical.Formula.atom a) = v a
• LO.Propositional.Classical.Formula.valAux v (LO.Propositional.Classical.Formula.natom a) = ∼v a
• LO.Propositional.Classical.Formula.valAux v LO.Propositional.Classical.Formula.verum = ⊤
• LO.Propositional.Classical.Formula.valAux v LO.Propositional.Classical.Formula.falsum = ⊥
• LO.Propositional.Classical.Formula.valAux v (p.and q) = LO.Propositional.Classical.Formula.valAux v p ⋏ LO.Propositional.Classical.Formula.valAux v q
• LO.Propositional.Classical.Formula.valAux v (p.or q) = LO.Propositional.Classical.Formula.valAux v p ⋎ LO.Propositional.Classical.Formula.valAux v q

theorem LO.Propositional.Classical.Formula.valAux_neg {α : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.DeMorgan F] (v : α → F) (p : LO.Propositional.Classical.Formula α) : LO.Propositional.Classical.Formula.valAux v (∼p) = ∼LO.Propositional.Classical.Formula.valAux v p

def LO.Propositional.Classical.Formula.val {α : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.DeMorgan F] (v : α → F) : LO.Propositional.Classical.Formula α →ˡᶜ F

Equations

• LO.Propositional.Classical.Formula.val v = { toTr := LO.Propositional.Classical.Formula.valAux v, map_top' := ⋯, map_bot' := ⋯, map_neg' := ⋯, map_imply' := ⋯, map_and' := ⋯, map_or' := ⋯ }

@[simp]

theorem LO.Propositional.Classical.Formula.val_atom {α : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.DeMorgan F] (v : α → F) {a : α} : (LO.Propositional.Classical.Formula.val v) (LO.Propositional.Classical.Formula.atom a) = v a

@[simp]

theorem LO.Propositional.Classical.Formula.val_natom {α : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.DeMorgan F] (v : α → F) {a : α} : (LO.Propositional.Classical.Formula.val v) (LO.Propositional.Classical.Formula.natom a) = ∼v a

structure LO.Propositional.Classical.Valuation (α : Type u_2) : Type u_2

• val : α → Prop

instance LO.Propositional.Classical.instCoeFunValuationForallProp {α : Type u_1} : CoeFun (LO.Propositional.Classical.Valuation α) fun (x : LO.Propositional.Classical.Valuation α) => α → Prop

Equations

• LO.Propositional.Classical.instCoeFunValuationForallProp = { coe := LO.Propositional.Classical.Valuation.val }

instance LO.Propositional.Classical.semantics {α : Type u_1} : LO.Semantics (LO.Propositional.Classical.Formula α) (LO.Propositional.Classical.Valuation α)

Equations

• LO.Propositional.Classical.semantics = { Realize := fun (v : LO.Propositional.Classical.Valuation α) => ⇑(LO.Propositional.Classical.Formula.val v.val) }

theorem LO.Propositional.Classical.models_iff_val {α : Type u_1} {v : LO.Propositional.Classical.Valuation α} {f : LO.Propositional.Classical.Formula α} : v ⊧ f ↔ (LO.Propositional.Classical.Formula.val v.val) f

instance LO.Propositional.Classical.instTarskiValuationFormula {α : Type u_1} : LO.Semantics.Tarski (LO.Propositional.Classical.Valuation α)

Equations

• LO.Propositional.Classical.instTarskiValuationFormula = LO.Semantics.Tarski.mk

@[simp]

theorem LO.Propositional.Classical.Formula.realize_atom {α : Type u_1} {v : LO.Propositional.Classical.Valuation α} {a : α} : v ⊧ LO.Propositional.Classical.Formula.atom a ↔ v.val a

@[simp]

theorem LO.Propositional.Classical.Formula.realize_natom {α : Type u_1} {v : LO.Propositional.Classical.Valuation α} {a : α} : v ⊧ LO.Propositional.Classical.Formula.natom a ↔ ¬v.val a