Contestability

This module formalizes:

• se100.assump.Contestability — Contestability

Contestability states that no contested causal or normative proposition is guaranteed framework-invariant at design time.

The assumption does not state that every contested proposition is actually framework-variant. It states that framework invariance for such a proposition cannot be established from a permitted design-time basis.

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

def SE.NeutralSubstrate.Assumptions.Contestability {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} (C : Logic.ConsequenceSystem L) (K : Classification.CausalNormativeClassification L) (c : K.Context) (G : Classification.InterpretiveStatusFixing L K.Context) (S : Substrate.SubstrateSystem L R) (F : Substrate.ReferentialFixing L R) (s : S.Carrier) (M : Framework.FrameworkSystem L.carrier) (D : DesignTimeGuaranteeSystem) : Prop

No contested causal or normative proposition is guaranteed framework-invariant at design time.

This formalizes the paper's condition that no p ∈ C_cn is guaranteed framework-invariant at design time.

Equations

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

@[simp]

theorem SE.NeutralSubstrate.Assumptions.contestability_iff {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {K : Classification.CausalNormativeClassification L} {c : K.Context} {G : Classification.InterpretiveStatusFixing L K.Context} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} {D : DesignTimeGuaranteeSystem} : Contestability C K c G S F s M D ↔ ∀ (p : L.Proposition), p ∈ Classification.ContestedCausalOrNormativeClass C K c G S F s → ¬GuaranteedAtDesignTime D (FrameworkRelative.FrameworkInvariantProposition C S s M p)

Contestability holds exactly when no member of the contested causal or normative class is guaranteed framework-invariant at design time.

theorem SE.NeutralSubstrate.Assumptions.not_guaranteedFrameworkInvariant_of_contestability {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {K : Classification.CausalNormativeClassification L} {c : K.Context} {G : Classification.InterpretiveStatusFixing L K.Context} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} {D : DesignTimeGuaranteeSystem} (hcontestability : Contestability C K c G S F s M D) {p : L.Proposition} (hp : p ∈ Classification.ContestedCausalOrNormativeClass C K c G S F s) : ¬GuaranteedAtDesignTime D (FrameworkRelative.FrameworkInvariantProposition C S s M p)

A contested causal or normative proposition is not guaranteed framework-invariant at design time.