Documentation

SE.CommonGround.Result.Independence

Independence of Common Ground from Admissibility #

Admissibility alone does not give common ground for a nontrivial fragment.

bareFrameworkSystem counts every non-logical admissibility condition as satisfied, so a framework is admissible exactly when it is satisfiable. In that system a commitment set is framework-compatible exactly when it is valid. Any nontrivial referential fragment therefore fails framework compatibility.

source
def SE.CommonGround.Result.bareFrameworkSystem (Atom : Type u) :
Framework.FrameworkSystem (Logic.language Atom).carrier

The framework system whose carrier is the theories themselves and in which every non-logical admissibility condition holds.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem SE.CommonGround.Result.admissible_bare_iff {Atom : Type u} {F : MathlibMini.Set (Logic.Formula Atom)} :
    Framework.AdmissibleFramework (Logic.semanticConsequenceSystem Atom) (bareFrameworkSystem Atom) F ↔ ∃ (w : Logic.Valuation Atom), Logic.Satisfies w F

    In the bare framework system, a framework is admissible exactly when it is satisfiable.

    source
    theorem SE.CommonGround.Result.satisfies_combine_iff {Atom : Type u} {w : Logic.Valuation Atom} {T U : Logic.Theory.CommitmentTheory (Logic.language Atom).carrier} :
    Logic.Satisfies w (Logic.Theory.combine T U) ↔ Logic.Satisfies w T ∧ Logic.Satisfies w U

    A valuation satisfies a combined theory exactly when it satisfies both parts.

    source
    theorem SE.CommonGround.Result.compatible_bare_iff_valid {Atom : Type u} {T : Logic.Theory.CommitmentTheory (Logic.language Atom).carrier} :
    NeutralSubstrate.FrameworkRelative.FrameworkCompatibleCommitmentSet (Logic.semanticConsequenceSystem Atom) (bareFrameworkSystem Atom) T ↔ ∀ (v : Logic.Valuation Atom), Logic.Satisfies v T

    In the bare framework system, a commitment set is framework-compatible exactly when every valuation satisfies it.

    source
    theorem SE.CommonGround.Result.not_compatible_bare_of_nontrivial {Atom : Type u} (P : Fragment.ReferentialFragment Atom) :
    ¬NeutralSubstrate.FrameworkRelative.FrameworkCompatibleCommitmentSet (Logic.semanticConsequenceSystem Atom) (bareFrameworkSystem Atom) P.commitments

    A nontrivial referential fragment is not framework-compatible when admissibility is the only condition on frameworks.