AUX-005. Entailment

This module defines the abstract consequence relation used by the Structural Explainability theory.

The consequence relation is intentionally independent of any particular proof calculus, model theory, decision procedure, or implementation.

The interface assumes:

• commitments entail their members;
• generalized cut;
• contradiction formation from a proposition and its object-language negation.

Generalized cut is a deliberate Tarskian consequence-system commitment. It supports removal of arbitrary collections of propositions that are already entailed by a theory, without assuming finiteness or enumeration.

Monotonicity is derived from generalized cut and entailment of theory members.

No explosion, excluded middle, negation introduction, completeness, decidability, or compactness principle is assumed.

structure SE.Logic.ConsequenceSystem (L : Language.PropositionalLanguage) : Type u

An abstract consequence system over a propositional language.

L supplies the object-language proposition carrier, negation operation, and distinguished contradiction proposition.

• entails : Theory.CommitmentTheory L.carrier → L.Proposition → Prop

  The consequence relation between a commitment theory and an object-language proposition.

• entailsOfMem {T : Theory.CommitmentTheory L.carrier} {p : L.Proposition} : p ∈ T → self.entails T p

  Every proposition explicitly contained in a commitment theory is entailed by that theory.

• cut {T U : Theory.CommitmentTheory L.carrier} {p : L.Proposition} : (∀ (q : L.carrier.Proposition), q ∈ U → self.entails T q) → self.entails U p → self.entails T p

  Generalized cut.

  If T entails every proposition in U, then every consequence of U is also a consequence of T.

• contradiction {T : Theory.CommitmentTheory L.carrier} {p : L.Proposition} : self.entails T p → self.entails T (L.neg p) → self.entails T L.bottom

  Entailment of both a proposition and its object-language negation entails the distinguished contradiction proposition.

theorem SE.Logic.ConsequenceSystem.entailsMono {L : Language.PropositionalLanguage} (C : ConsequenceSystem L) {T U : Theory.CommitmentTheory L.carrier} {p : L.Proposition} (hTU : T ⊆ U) (hp : C.entails T p) : C.entails U p

Entailment is monotone under extension of the commitment theory.