Vocabulary #

A vocabulary is a set of atoms.

A formula lies in a vocabulary when every atom occurring in it belongs to the vocabulary. A theory lies in a vocabulary when all of its members do.

Valuations that agree on a vocabulary give every formula in that vocabulary the same truth value (eval_congr). That is the only fact about vocabularies the later results need from the semantics.

source

@[reducible, inline]

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

Type u

A vocabulary is a set of atoms.

Equations

SE.CommonGround.Logic.Vocabulary Atom = MathlibMini.Set Atom

Instances For

source

def SE.CommonGround.Logic.VocabularyDisjoint {Atom : Type u} (V W : Vocabulary Atom) :

Prop

Two vocabularies are disjoint when no atom belongs to both.

Equations

SE.CommonGround.Logic.VocabularyDisjoint V W = ∀ (a : Atom), a ∈ V → a ∈ W → False

Instances For

source

def SE.CommonGround.Logic.FormulaIn {Atom : Type u} (V : Vocabulary Atom) :

Formula Atom → Prop

A formula lies in a vocabulary when every atom occurring in it belongs to the vocabulary.

Equations

SE.CommonGround.Logic.FormulaIn V (SE.CommonGround.Logic.Formula.atom a) = (a ∈ V)
SE.CommonGround.Logic.FormulaIn V SE.CommonGround.Logic.Formula.bot = True
SE.CommonGround.Logic.FormulaIn V f.neg = SE.CommonGround.Logic.FormulaIn V f
SE.CommonGround.Logic.FormulaIn V (f.conj g) = (SE.CommonGround.Logic.FormulaIn V f ∧ SE.CommonGround.Logic.FormulaIn V g)

Instances For

source

def SE.CommonGround.Logic.TheoryIn {Atom : Type u} (V : Vocabulary Atom) (T : MathlibMini.Set (Formula Atom)) :

Prop

A theory lies in a vocabulary when every member lies in the vocabulary.

Equations

SE.CommonGround.Logic.TheoryIn V T = ∀ (f : SE.CommonGround.Logic.Formula Atom), f ∈ T → SE.CommonGround.Logic.FormulaIn V f

Instances For

source

theorem SE.CommonGround.Logic.eval_congr {Atom : Type u} {V : Vocabulary Atom} {v w : Valuation Atom} (hagree : ∀ (a : Atom), a ∈ V → (v a ↔ w a)) (f : Formula Atom) :

FormulaIn V f → (eval v f ↔ eval w f)

Valuations that agree on a vocabulary agree on every formula in it.

source

theorem SE.CommonGround.Logic.satisfies_congr {Atom : Type u} {V : Vocabulary Atom} {v w : Valuation Atom} (hagree : ∀ (a : Atom), a ∈ V → (v a ↔ w a)) {T : MathlibMini.Set (Formula Atom)} (hT : TheoryIn V T) :

Satisfies v T ↔ Satisfies w T

Valuations that agree on a vocabulary satisfy the same theories over it.