Documentation

SE.NeutralSubstrate.Assumptions.ReferentialCommonGround

Referential Common Ground #

This module formalizes:

Referential common ground requires the substrate's referential commitments to remain compatible with every admissible framework.

It also requires that adjoining any permitted attribution proposition to the referential commitments remains compatible with every admissible framework.

The quantification ranges over the complete framework class, not merely over frameworks known when the substrate is designed. No enumeration of that class is assumed.

source
def SE.NeutralSubstrate.Assumptions.ReferentialCommonGround {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} (C : Logic.ConsequenceSystem L) (S : Substrate.SubstrateSystem L R) (F : Substrate.ReferentialFixing L R) (A : Attribution.AttributionSystem L) (B : Attribution.AttributionalBasisFixing C A) (s : S.Carrier) (M : Framework.FrameworkSystem L.carrier) :
Prop

Referential common ground holds when:

  1. the substrate's referential commitments are compatible with every admissible framework; and
  2. adjoining any permitted attribution proposition to those referential commitments remains compatible with every admissible framework.

The second condition formalizes:

Sref ∪ {asserts x φ} ∪ F ⊬ ⊥.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem SE.NeutralSubstrate.Assumptions.referentialCommonGround_iff {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {A : Attribution.AttributionSystem L} {B : Attribution.AttributionalBasisFixing C A} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} :
    ReferentialCommonGround C S F A B s M ↔ FrameworkRelative.FrameworkCompatibleCommitmentSet C M (Substrate.ReferentialCommitments C S F s) ∧ ∀ (p : L.Proposition), Attribution.PermittedAttributionProposition C S F A B s p → FrameworkRelative.FrameworkCompatibleCommitmentSet C M (Logic.Theory.adjoin (Substrate.ReferentialCommitments C S F s) p)

    Referential common ground holds exactly when the referential commitments and each permitted-attribution extension are framework-compatible.

    source
    theorem SE.NeutralSubstrate.Assumptions.referentialCommitments_compatible_of_referentialCommonGround {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {A : Attribution.AttributionSystem L} {B : Attribution.AttributionalBasisFixing C A} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} (hcommonGround : ReferentialCommonGround C S F A B s M) :
    FrameworkRelative.FrameworkCompatibleCommitmentSet C M (Substrate.ReferentialCommitments C S F s)

    The substrate's referential commitments are compatible with every admissible framework.

    source
    theorem SE.NeutralSubstrate.Assumptions.permittedAttribution_compatible_of_referentialCommonGround {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {A : Attribution.AttributionSystem L} {B : Attribution.AttributionalBasisFixing C A} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} (hcommonGround : ReferentialCommonGround C S F A B s M) {p : L.Proposition} (hp : Attribution.PermittedAttributionProposition C S F A B s p) :
    FrameworkRelative.FrameworkCompatibleCommitmentSet C M (Logic.Theory.adjoin (Substrate.ReferentialCommitments C S F s) p)

    Adjoining a permitted attribution proposition to the referential commitments produces a framework-compatible commitment set.

    source
    theorem SE.NeutralSubstrate.Assumptions.consistent_referentialCommitments_of_referentialCommonGround {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {A : Attribution.AttributionSystem L} {B : Attribution.AttributionalBasisFixing C A} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} (hcommonGround : ReferentialCommonGround C S F A B s M) {framework : M.Carrier} (hframework : framework ∈ Framework.FrameworkClass C M) :
    Logic.Consistent C (Logic.Theory.combine (Substrate.ReferentialCommitments C S F s) (M.commitments framework))

    The referential commitments remain consistent with the commitments of any admissible framework.

    source
    theorem SE.NeutralSubstrate.Assumptions.consistent_permittedAttribution_of_referentialCommonGround {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {A : Attribution.AttributionSystem L} {B : Attribution.AttributionalBasisFixing C A} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} (hcommonGround : ReferentialCommonGround C S F A B s M) {p : L.Proposition} (hp : Attribution.PermittedAttributionProposition C S F A B s p) {framework : M.Carrier} (hframework : framework ∈ Framework.FrameworkClass C M) :
    Logic.Consistent C (Logic.Theory.combine (Logic.Theory.adjoin (Substrate.ReferentialCommitments C S F s) p) (M.commitments framework))

    The referential commitments together with any permitted attribution proposition remain consistent with the commitments of any admissible framework.