Scope Dichotomy

Every framework is either neutral on a vocabulary V or conflicts with some satisfiable theory over V.

The second case is the exact witness that the scope condition fails. It names a concrete satisfiable theory over V that the framework cannot coexist with. Whether such a theory is the referential commitment set of a given fragment is a question about that fragment, not something this module settles.

theorem SE.CommonGround.Scope.dichotomy {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)

Either F is neutral on V, or some satisfiable theory over V is not jointly satisfiable with F.