Attribution and Common Ground

This module formalizes:

• se100.remark.AttributionCommonGround — Attribution and Common Ground

A permitted attribution proposition asserts x φ commits the substrate to the attribution by x, not to the asserted proposition φ.

Because a permitted attribution proposition is already entailed by the substrate's referential commitments, adjoining it adds no independent commitment. For every framework, the extended theory entails contradiction exactly when the unextended theory entails contradiction.

Referential Common Ground therefore ensures that the referential commitments, a permitted attribution proposition, and every admissible framework remain jointly consistent.

An admissible framework may reject φ without rejecting that x asserted φ. This module does not infer φ from asserts x φ.

No decidability, finiteness, enumeration, or effective search procedure is assumed.

theorem SE.NeutralSubstrate.Attribution.entailsBottom_combine_adjoin_iff_of_entails {L : Logic.Language.PropositionalLanguage} (C : Logic.ConsequenceSystem L) {T U : Logic.Theory.CommitmentTheory L.carrier} {p : L.Proposition} (hp : C.entails T p) : C.entails (Logic.Theory.combine (Logic.Theory.adjoin T p) U) L.bottom ↔ C.entails (Logic.Theory.combine T U) L.bottom

Adjoining a proposition already entailed by a commitment theory does not change whether its combination with another theory entails contradiction.

The forward direction uses generalized cut. The reverse direction follows from monotonicity.

theorem SE.NeutralSubstrate.Attribution.entailsBottom_permittedAttribution_iff {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {A : AttributionSystem L} (B : AttributionalBasisFixing C A) {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} {p : L.Proposition} (hp : PermittedAttributionProposition C S F A B s p) (framework : M.Carrier) : C.entails (Logic.Theory.combine (Logic.Theory.adjoin (Substrate.ReferentialCommitments C S F s) p) (M.commitments framework)) L.bottom ↔ C.entails (Logic.Theory.combine (Substrate.ReferentialCommitments C S F s) (M.commitments framework)) L.bottom

Adjoining a permitted attribution proposition to the referential commitments does not change whether the resulting theory combined with a framework entails contradiction.

This theorem does not require the selected framework to be admissible; the consequence equivalence follows solely from the permitted attribution proposition already being entailed by the referential commitments.

theorem SE.NeutralSubstrate.Attribution.consistent_permittedAttribution_of_commonGround {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {A : AttributionSystem L} {B : AttributionalBasisFixing C A} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} (hcommonGround : Assumptions.ReferentialCommonGround C S F A B s M) {p : L.Proposition} (hp : 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))

Under Referential Common Ground, adjoining a permitted attribution proposition to the referential commitments remains consistent with every admissible framework.