Documentation

SE.Logic.Consistency

AUX-006. Consistency #

This module defines consistency for a commitment theory.

A commitment theory is consistent exactly when it does not entail the distinguished object-language contradiction proposition.

Consistency is proposition-valued. No Boolean decision procedure, decidability assumption, or consistency-by-construction restriction is introduced.

source
def SE.Logic.Consistent {L : Language.PropositionalLanguage} (C : ConsequenceSystem L) (T : Theory.CommitmentTheory L.carrier) :
Prop

A commitment theory is consistent when it does not entail the distinguished object-language contradiction proposition.

Equations
Instances For
    source
    theorem SE.Logic.not_entailsBottom_of_consistent {L : Language.PropositionalLanguage} {C : ConsequenceSystem L} {T : Theory.CommitmentTheory L.carrier} (hconsistent : Consistent C T) :
    ¬C.entails T L.bottom

    Consistency means that the commitment theory does not entail contradiction.

    source
    theorem SE.Logic.consistent_of_not_entailsBottom {L : Language.PropositionalLanguage} {C : ConsequenceSystem L} {T : Theory.CommitmentTheory L.carrier} (hnotBottom : ¬C.entails T L.bottom) :
    Consistent C T

    Failure to entail contradiction establishes consistency.