Classical Semantics

Truth, satisfaction and semantic consequence for Formula.

A valuation assigns a Lean proposition to each atom. eval extends a valuation to all formulas. A theory is satisfied by a valuation when every member is true under it. A theory semantically entails a formula when every valuation that satisfies the theory makes the formula true.

This semantics is classical. It is stronger than the abstract consequence system in Neutral Substrate requires, for example explosion holds. Results in this repository that depend on classical features are therefore results about this instance.

@[reducible, inline]

abbrev SE.CommonGround.Logic.Valuation (Atom : Type u) : Type u

A valuation assigns a Lean proposition to each atom.

Equations

• SE.CommonGround.Logic.Valuation Atom = (Atom → Prop)

def SE.CommonGround.Logic.eval {Atom : Type u} (v : Valuation Atom) : Formula Atom → Prop

Truth of a formula under a valuation.

Equations

• SE.CommonGround.Logic.eval v (SE.CommonGround.Logic.Formula.atom a) = v a
• SE.CommonGround.Logic.eval v SE.CommonGround.Logic.Formula.bot = False
• SE.CommonGround.Logic.eval v f.neg = ¬SE.CommonGround.Logic.eval v f
• SE.CommonGround.Logic.eval v (f.conj g) = (SE.CommonGround.Logic.eval v f ∧ SE.CommonGround.Logic.eval v g)

theorem SE.CommonGround.Logic.eval_atom {Atom : Type u} (v : Valuation Atom) (a : Atom) : eval v (Formula.atom a) ↔ v a

An atom is true under a valuation exactly when the valuation makes it true.

theorem SE.CommonGround.Logic.eval_bot {Atom : Type u} (v : Valuation Atom) : eval v Formula.bot ↔ False

The contradiction is false under any valuation.

theorem SE.CommonGround.Logic.eval_neg {Atom : Type u} (v : Valuation Atom) (f : Formula Atom) : eval v f.neg ↔ ¬eval v f

The negation of a formula is true under a valuation exactly when the formula is false under it.

theorem SE.CommonGround.Logic.eval_conj {Atom : Type u} (v : Valuation Atom) (f g : Formula Atom) : eval v (f.conj g) ↔ eval v f ∧ eval v g

The conjunction of two formulas is true under a valuation exactly when both formulas are true under it.

def SE.CommonGround.Logic.Satisfies {Atom : Type u} (v : Valuation Atom) (T : MathlibMini.Set (Formula Atom)) : Prop

A valuation satisfies a theory when every member of the theory is true under it.

Equations

• SE.CommonGround.Logic.Satisfies v T = ∀ (f : SE.CommonGround.Logic.Formula Atom), f ∈ T → SE.CommonGround.Logic.eval v f

def SE.CommonGround.Logic.SemanticEntails {Atom : Type u} (T : MathlibMini.Set (Formula Atom)) (f : Formula Atom) : Prop

A theory semantically entails a formula when every valuation satisfying the theory makes the formula true.

Equations

• SE.CommonGround.Logic.SemanticEntails T f = ∀ (v : SE.CommonGround.Logic.Valuation Atom), SE.CommonGround.Logic.Satisfies v T → SE.CommonGround.Logic.eval v f

theorem SE.CommonGround.Logic.satisfies_union_iff {Atom : Type u} {v : Valuation Atom} {T U : MathlibMini.Set (Formula Atom)} : Satisfies v (T ∪ U) ↔ Satisfies v T ∧ Satisfies v U

A valuation satisfies a union of theories exactly when it satisfies both.

theorem SE.CommonGround.Logic.satisfies_mono {Atom : Type u} {v : Valuation Atom} {T U : MathlibMini.Set (Formula Atom)} (hTU : T ⊆ U) (h : Satisfies v U) : Satisfies v T

Satisfying a larger theory implies satisfying any subset of it.

theorem SE.CommonGround.Logic.semanticEntails_bot_iff {Atom : Type u} {T : MathlibMini.Set (Formula Atom)} : SemanticEntails T Formula.bot ↔ ∀ (v : Valuation Atom), ¬Satisfies v T

A theory semantically entails the contradiction exactly when no valuation satisfies it.