Interface of a Framework on a Vocabulary

The interface of a framework F on a vocabulary V is the set of valuations of V that F permits: those that extend to a model of F.

satisfiable_union_iff_permits reduces compatibility of a theory over V with F to a question about this interface alone.

valuationDiagram V u is the theory over V that says exactly what the valuation u says about the atoms of V.

def SE.CommonGround.Scope.Permits {Atom : Type u} (V : Logic.Vocabulary Atom) (F : MathlibMini.Set (Logic.Formula Atom)) (u : Logic.Valuation Atom) : Prop

F permits u on V when some model of F agrees with u on V.

Equations

• SE.CommonGround.Scope.Permits V F u = ∃ (w : SE.CommonGround.Logic.Valuation Atom), SE.CommonGround.Logic.Satisfies w F ∧ ∀ (a : Atom), a ∈ V → (w a ↔ u a)

theorem SE.CommonGround.Scope.satisfiable_union_iff_permits {Atom : Type u} {V : Logic.Vocabulary Atom} {R F : MathlibMini.Set (Logic.Formula Atom)} (hR : Logic.TheoryIn V R) : (∃ (w : Logic.Valuation Atom), Logic.Satisfies w (R ∪ F)) ↔ ∃ (u : Logic.Valuation Atom), Logic.Satisfies u R ∧ Permits V F u

A theory R over V is jointly satisfiable with F exactly when F permits some valuation that satisfies R.

def SE.CommonGround.Scope.valuationDiagram {Atom : Type u} (V : Logic.Vocabulary Atom) (u : Logic.Valuation Atom) : MathlibMini.Set (Logic.Formula Atom)

The theory over V consisting of atom a for each a in V that u makes true and neg (atom a) for each a in V that u makes false.

Equations

• One or more equations did not get rendered due to their size.

theorem SE.CommonGround.Scope.valuationDiagram_in_vocabulary {Atom : Type u} {V : Logic.Vocabulary Atom} {u : Logic.Valuation Atom} : Logic.TheoryIn V (valuationDiagram V u)

The diagram of u on V lies in V.

theorem SE.CommonGround.Scope.satisfies_valuationDiagram {Atom : Type u} {V : Logic.Vocabulary Atom} {u : Logic.Valuation Atom} : Logic.Satisfies u (valuationDiagram V u)

The valuation u satisfies its own diagram.