Scope Condition on Frameworks

NeutralOn V F says the framework F permits every valuation of the vocabulary V. It mentions only V and F. It does not mention any fragment's commitments, so it is characterized independently of compatibility with them.

Two facts relate it to compatibility.

• neutralOn_iff_compatible: F is neutral on V exactly when F is compatible with every satisfiable theory over V. No weaker condition on F alone gives compatibility for every fragment over V. For one fixed fragment, weaker conditions can suffice, as satisfiable_union_iff_permits shows.
• neutralOn_of_avoids: a framework written entirely in a vocabulary disjoint from V is neutral on V, provided it is satisfiable. Disjointness can be checked by reading the framework.

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

F is neutral on V when it permits every valuation of V.

Equations

• SE.CommonGround.Scope.NeutralOn V F = ∀ (u : SE.CommonGround.Logic.Valuation Atom), SE.CommonGround.Scope.Permits V F u

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

F avoids V when F lies entirely in some vocabulary disjoint from V.

Equations

• SE.CommonGround.Scope.AvoidsVocabulary V F = ∃ (W : SE.CommonGround.Logic.Vocabulary Atom), SE.CommonGround.Logic.TheoryIn W F ∧ SE.CommonGround.Logic.VocabularyDisjoint V W

theorem SE.CommonGround.Scope.neutralOn_of_avoids {Atom : Type u} {V : Logic.Vocabulary Atom} {F : MathlibMini.Set (Logic.Formula Atom)} (havoids : AvoidsVocabulary V F) (hsat : ∃ (w : Logic.Valuation Atom), Logic.Satisfies w F) : NeutralOn V F

A satisfiable framework that avoids V is neutral on V.

theorem SE.CommonGround.Scope.neutralOn_iff_compatible {Atom : Type u} {V : Logic.Vocabulary Atom} {F : MathlibMini.Set (Logic.Formula Atom)} : NeutralOn V F ↔ ∀ (R : MathlibMini.Set (Logic.Formula Atom)), Logic.TheoryIn V R → (∃ (v : Logic.Valuation Atom), Logic.Satisfies v R) → ∃ (w : Logic.Valuation Atom), Logic.Satisfies w (R ∪ F)

F is neutral on V exactly when F is jointly satisfiable with every satisfiable theory over V.