Semantic Consequence System

Semantic consequence on Formula as an instance of the abstract SE.Logic.ConsequenceSystem from Common Ground.

The three required properties hold:

• every member of a theory is entailed by it;
• generalized cut;
• a formula and its negation entail the contradiction.

Consistency in this instance coincides with satisfiability. That equivalence is the bridge the later joint-consistency results use.

def SE.CommonGround.Logic.semanticConsequenceSystem (Atom : Type u) : Logic.ConsequenceSystem (language Atom)

Semantic consequence over Formula Atom, as a Common Ground consequence system for language Atom.

Equations

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

theorem SE.CommonGround.Logic.consistent_iff_satisfiable {Atom : Type u} {T : Logic.Theory.CommitmentTheory (language Atom).carrier} : Logic.Consistent (semanticConsequenceSystem Atom) T ↔ ∃ (v : Valuation Atom), Satisfies v T

In the semantic consequence system, a theory is consistent exactly when some valuation satisfies it.