Joint Consistency over Disjoint Vocabularies

If a theory over V and a theory over W are each satisfiable and V and W are disjoint, their union is satisfiable.

Common Ground's consequence system is abstract and has no vocabularies, so this property cannot be stated there. Here it is a theorem about the propositional instance. The construction takes one valuation on V and the other outside V.

def SE.CommonGround.Logic.splice {Atom : Type u} (V : Vocabulary Atom) (v₁ v₂ : Valuation Atom) : Valuation Atom

The valuation that agrees with v₁ on V and with v₂ outside V.

Equations

• SE.CommonGround.Logic.splice V v₁ v₂ a = (a ∈ V ∧ v₁ a ∨ ¬a ∈ V ∧ v₂ a)

theorem SE.CommonGround.Logic.splice_iff_of_mem {Atom : Type u} {V : Vocabulary Atom} {v₁ v₂ : Valuation Atom} {a : Atom} (ha : a ∈ V) : splice V v₁ v₂ a ↔ v₁ a

On V, the spliced valuation agrees with v₁.

theorem SE.CommonGround.Logic.splice_iff_of_not_mem {Atom : Type u} {V : Vocabulary Atom} {v₁ v₂ : Valuation Atom} {a : Atom} (ha : ¬a ∈ V) : splice V v₁ v₂ a ↔ v₂ a

Outside V, the spliced valuation agrees with v₂.

theorem SE.CommonGround.Logic.satisfiable_union_of_disjoint {Atom : Type u} {V W : Vocabulary Atom} (hdisjoint : VocabularyDisjoint V W) {T U : MathlibMini.Set (Formula Atom)} (hT : TheoryIn V T) (hU : TheoryIn W U) (hTsat : ∃ (v : Valuation Atom), Satisfies v T) (hUsat : ∃ (v : Valuation Atom), Satisfies v U) : ∃ (v : Valuation Atom), Satisfies v (T ∪ U)

Satisfiable theories over disjoint vocabularies have a satisfiable union.