Extension Stability

This module formalizes:

• se100.def.ExtensionStability — Extension Stability

A substrate satisfies extension stability when its commitments remain consistent with the commitments of every admissible framework.

For every admissible framework F, the combined commitment theory satisfies:

S ∪ F ⊬ ⊥.

Here, extension refers to combining a substrate with a framework. It does not refer to changing or enlarging the intrinsic framework class.

No decidability, finiteness, enumeration, or effective search procedure for the framework class is assumed.

def SE.NeutralSubstrate.Neutrality.ExtensionStability {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} (C : Logic.ConsequenceSystem L) (S : Substrate.SubstrateSystem L R) (s : S.Carrier) (M : Framework.FrameworkSystem L.carrier) : Prop

A substrate satisfies extension stability when its combined commitment theory with every admissible framework remains consistent.

This formalizes the paper's condition:

S ∪ F ⊬ ⊥

for every admissible framework F.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SE.NeutralSubstrate.Neutrality.extensionStability_iff {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} : ExtensionStability C S s M ↔ ∀ (framework : M.Carrier), framework ∈ Framework.FrameworkClass C M → Logic.Consistent C (FrameworkRelative.SubstrateFrameworkCommitments S s M framework)

A substrate satisfies extension stability exactly when every admissible substrate-framework commitment theory remains consistent.

theorem SE.NeutralSubstrate.Neutrality.consistent_substrateFrameworkCommitments_of_extensionStability {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} (hstability : ExtensionStability C S s M) {framework : M.Carrier} (hframework : framework ∈ Framework.FrameworkClass C M) : Logic.Consistent C (FrameworkRelative.SubstrateFrameworkCommitments S s M framework)

Extension stability supplies consistency for the substrate combined with any selected admissible framework.