Documentation

SE.NeutralSubstrate.Neutrality.ByDesign

Neutrality by Design #

This module formalizes:

A substrate is neutral when it satisfies both:

A substrate is neutral by design when its neutrality is guaranteed at design time. The guarantee ranges over the complete intrinsic framework class through the quantified definitions of interpretive non-commitment and extension stability.

The design-time guarantee must arise from a permitted design-time basis. It must not rest on enumerating only the admissible frameworks known when the substrate is designed.

source
def SE.NeutralSubstrate.Neutrality.Neutral {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 is neutral when it satisfies interpretive non-commitment and extension stability.

Equations
Instances For
    source
    @[simp]
    theorem SE.NeutralSubstrate.Neutrality.neutral_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} :
    Neutral C S s M ↔ InterpretiveNonCommitment C S s M ∧ ExtensionStability C S s M

    A substrate is neutral exactly when it satisfies interpretive non-commitment and extension stability.

    source
    theorem SE.NeutralSubstrate.Neutrality.interpretiveNonCommitment_of_neutral {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} (hneutral : Neutral C S s M) :
    InterpretiveNonCommitment C S s M

    A neutral substrate satisfies interpretive non-commitment.

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

    A neutral substrate satisfies extension stability.

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

    A substrate is neutral by design when its neutrality is guaranteed by a permitted design-time basis.

    Equations
    Instances For
      source
      @[simp]
      theorem SE.NeutralSubstrate.Neutrality.neutralByDesign_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} {D : DesignTimeGuaranteeSystem} :
      NeutralByDesign C S s M D ↔ GuaranteedAtDesignTime D (Neutral C S s M)

      A substrate is neutral by design exactly when a permitted design-time basis establishes its neutrality.

      source
      theorem SE.NeutralSubstrate.Neutrality.neutral_of_neutralByDesign {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} {D : DesignTimeGuaranteeSystem} (hdesign : NeutralByDesign C S s M D) :
      Neutral C S s M

      Every substrate that is neutral by design is neutral.

      source
      theorem SE.NeutralSubstrate.Neutrality.interpretiveNonCommitment_of_neutralByDesign {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} {D : DesignTimeGuaranteeSystem} (hdesign : NeutralByDesign C S s M D) :
      InterpretiveNonCommitment C S s M

      Neutrality by design entails interpretive non-commitment.

      source
      theorem SE.NeutralSubstrate.Neutrality.extensionStability_of_neutralByDesign {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} {D : DesignTimeGuaranteeSystem} (hdesign : NeutralByDesign C S s M D) :
      ExtensionStability C S s M

      Neutrality by design entails extension stability.