def LO.Propositional.Classical.Formula.valAux {α : Type u_1} {F : Type u_2} [LogicalConnective F] (v : α → F) : 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 (φ.and ψ) = LO.Propositional.Classical.Formula.valAux v φ ⋏ LO.Propositional.Classical.Formula.valAux v ψ
• LO.Propositional.Classical.Formula.valAux v (φ.or ψ) = LO.Propositional.Classical.Formula.valAux v φ ⋎ LO.Propositional.Classical.Formula.valAux v ψ

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

def LO.Propositional.Classical.Formula.val {α : Type u_1} {F : Type u_2} [LogicalConnective F] [DeMorgan F] (v : α → F) : 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} [LogicalConnective F] [DeMorgan F] (v : α → F) {a : α} : (val v) (atom a) = v a

@[simp]

theorem LO.Propositional.Classical.Formula.val_natom {α : Type u_1} {F : Type u_2} [LogicalConnective F] [DeMorgan F] (v : α → F) {a : α} : (val v) (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 (Valuation α) fun (x : Valuation α) => α → Prop

Equations

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

instance LO.Propositional.Classical.semantics {α : Type u_1} : Semantics (Formula α) (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 : Valuation α} {f : Formula α} : v ⊧ f ↔ (Formula.val v.val) f

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

@[simp]

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

@[simp]

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