Object-Level Causal or Normative Commitment

This module formalizes:

• se100.def.ObjectLevelCausalNormativeCommitment — Object-Level Causal or Normative Commitment

An object-level causal or normative proposition is an object-level interpretive proposition whose content is classified as causal or normative in the relevant accountability context.

An object-level causal or normative commitment is a substrate-layer commitment to such a proposition, rather than a commitment to an attribution proposition about it.

No decidability, exhaustiveness, or computational classification assumption is imposed.

def SE.NeutralSubstrate.Interpretation.ObjectLevelCausalOrNormativeProposition {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} (K : Classification.CausalNormativeClassification L) (c : K.Context) (A : Attribution.AttributionSystem L) (I : ObjectLevelInterpretation L R) (S : Substrate.SubstrateSystem L R) (s : S.Carrier) (p : L.Proposition) : Prop

An object-level causal or normative proposition is an object-level interpretive proposition whose content is classified as causal or normative in the selected accountability context.

Equations

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

def SE.NeutralSubstrate.Interpretation.ObjectLevelCausalOrNormativeCommitment {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} (C : Logic.ConsequenceSystem L) (K : Classification.CausalNormativeClassification L) (c : K.Context) (A : Attribution.AttributionSystem L) (I : ObjectLevelInterpretation L R) (S : Substrate.SubstrateSystem L R) (s : S.Carrier) (p : L.Proposition) : Prop

An object-level causal or normative commitment is a substrate-layer commitment to an object-level causal or normative proposition.

Equations

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

@[simp]

theorem SE.NeutralSubstrate.Interpretation.objectLevelCausalOrNormativeCommitment_iff {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {K : Classification.CausalNormativeClassification L} {c : K.Context} {A : Attribution.AttributionSystem L} {I : ObjectLevelInterpretation L R} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} {p : L.Proposition} : ObjectLevelCausalOrNormativeCommitment C K c A I S s p ↔ Substrate.SubstrateCommitment C S s p ∧ ObjectLevelCausalOrNormativeProposition K c A I S s p

A proposition is an object-level causal or normative commitment exactly when the substrate commits to it and it is an object-level causal or normative proposition.

theorem SE.NeutralSubstrate.Interpretation.substrateCommitment_of_objectLevelCausalOrNormativeCommitment {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {K : Classification.CausalNormativeClassification L} {c : K.Context} {A : Attribution.AttributionSystem L} {I : ObjectLevelInterpretation L R} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} {p : L.Proposition} (hp : ObjectLevelCausalOrNormativeCommitment C K c A I S s p) : Substrate.SubstrateCommitment C S s p

Every object-level causal or normative commitment is a substrate-layer commitment.

theorem SE.NeutralSubstrate.Interpretation.objectLevelInterpretiveProposition_of_objectLevelCausalOrNormativeCommitment {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {K : Classification.CausalNormativeClassification L} {c : K.Context} {A : Attribution.AttributionSystem L} {I : ObjectLevelInterpretation L R} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} {p : L.Proposition} (hp : ObjectLevelCausalOrNormativeCommitment C K c A I S s p) : ObjectLevelInterpretiveProposition A I S s p

Every object-level causal or normative commitment concerns the referents fixed by the substrate.

theorem SE.NeutralSubstrate.Interpretation.causalOrNormativeProposition_of_objectLevelCausalOrNormativeCommitment {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {K : Classification.CausalNormativeClassification L} {c : K.Context} {A : Attribution.AttributionSystem L} {I : ObjectLevelInterpretation L R} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} {p : L.Proposition} (hp : ObjectLevelCausalOrNormativeCommitment C K c A I S s p) : Classification.CausalOrNormativeProposition K c p

Every object-level causal or normative commitment has causal or normative content in the selected accountability context.