Contested Causal or Normative Propositions

This module formalizes:

• se100.def.ContestedCausalNormative — Contested Causal or Normative Proposition

A causal or normative proposition is contested in an accountability context when its acceptance, rejection, interpretation, or application is not fixed by the substrate's referential commitments.

The paper does not reduce this determination to entailment, syntax, or a formal decision procedure. This module therefore represents the fixing of a proposition's interpretive status as an abstract, context-relative relation.

A contested proposition may vary across admissible frameworks. The definition does not require evidence of actual variation between two frameworks. Actual opposed entailments are represented separately by FrameworkVariantProposition.

No decidability, finiteness, enumeration, or computational classification assumption is imposed.

structure SE.NeutralSubstrate.Classification.InterpretiveStatusFixing (L : Logic.Language.PropositionalLanguage) (Context : Type x) : Type (max u x)

An abstract account of whether the interpretive status of a proposition is fixed by a commitment theory in an accountability context.

fixedBy c T p states that the acceptance, rejection, interpretation, or application relevant to proposition p is fixed by commitment theory T in context c.

• fixedBy : Context → Logic.Theory.CommitmentTheory L.carrier → L.Proposition → Prop

  Whether a commitment theory fixes the relevant interpretive status of a proposition in an accountability context.

def SE.NeutralSubstrate.Classification.ContestedCausalOrNormativeProposition {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} (C : Logic.ConsequenceSystem L) (K : CausalNormativeClassification L) (c : K.Context) (G : InterpretiveStatusFixing L K.Context) (S : Substrate.SubstrateSystem L R) (F : Substrate.ReferentialFixing L R) (s : S.Carrier) (p : L.Proposition) : Prop

A proposition is contested causal or normative when:

1. it is classified as causal or normative in the selected accountability context; and
2. its relevant interpretive status is not fixed by the substrate's referential commitments.

The definition does not assert that two admissible frameworks actually produce opposed entailments.

Equations

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

def SE.NeutralSubstrate.Classification.ContestedCausalOrNormativeClass {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} (C : Logic.ConsequenceSystem L) (K : CausalNormativeClassification L) (c : K.Context) (G : InterpretiveStatusFixing L K.Context) (S : Substrate.SubstrateSystem L R) (F : Substrate.ReferentialFixing L R) (s : S.Carrier) : MathlibMini.Set L.Proposition

The class C_cn of contested causal or normative propositions for the selected substrate and accountability context.

Equations

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

@[simp]

theorem SE.NeutralSubstrate.Classification.contestedCausalOrNormativeProposition_iff {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {K : CausalNormativeClassification L} {c : K.Context} {G : InterpretiveStatusFixing L K.Context} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {s : S.Carrier} {p : L.Proposition} : ContestedCausalOrNormativeProposition C K c G S F s p ↔ CausalOrNormativeProposition K c p ∧ ¬G.fixedBy c (Substrate.ReferentialCommitments C S F s) p

A proposition is contested causal or normative exactly when it is causal or normative and its interpretive status is not fixed by the referential commitments.

@[simp]

theorem SE.NeutralSubstrate.Classification.mem_contestedCausalOrNormativeClass_iff {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {K : CausalNormativeClassification L} {c : K.Context} {G : InterpretiveStatusFixing L K.Context} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {s : S.Carrier} {p : L.Proposition} : p ∈ ContestedCausalOrNormativeClass C K c G S F s ↔ ContestedCausalOrNormativeProposition C K c G S F s p

Membership in C_cn is equivalent to being a contested causal or normative proposition.

theorem SE.NeutralSubstrate.Classification.causalOrNormativeProposition_of_contestedCausalOrNormativeProposition {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {K : CausalNormativeClassification L} {c : K.Context} {G : InterpretiveStatusFixing L K.Context} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {s : S.Carrier} {p : L.Proposition} (hp : ContestedCausalOrNormativeProposition C K c G S F s p) : CausalOrNormativeProposition K c p

Every contested causal or normative proposition is classified as causal or normative in the selected accountability context.

theorem SE.NeutralSubstrate.Classification.not_fixedBy_of_contestedCausalOrNormativeProposition {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {K : CausalNormativeClassification L} {c : K.Context} {G : InterpretiveStatusFixing L K.Context} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {s : S.Carrier} {p : L.Proposition} (hp : ContestedCausalOrNormativeProposition C K c G S F s p) : ¬G.fixedBy c (Substrate.ReferentialCommitments C S F s) p

The interpretive status of a contested causal or normative proposition is not fixed by the substrate's referential commitments.