Interpretive Non-Commitment

This module formalizes:

• se100.def.InterpretiveNonCommitment — Interpretive Non-Commitment

A substrate satisfies interpretive non-commitment when it makes no substrate-layer commitment to either side of a framework-variant proposition.

For every proposition p that is framework-variant with respect to the substrate and framework class, the substrate entails neither p nor its object-language negation ¬p.

The definition uses this explicit two-sided condition directly. It does not assume that the object-language negation of every framework-variant proposition is itself framework-variant, because the abstract language does not impose a double-negation law.

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

def SE.NeutralSubstrate.Neutrality.InterpretiveNonCommitment {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 interpretive non-commitment when every framework-variant proposition is absent from the substrate's commitments in both its positive and object-language-negated forms.

This formalizes the paper's condition:

S ⊬ p and S ⊬ ¬p

whenever p is framework-variant with respect to S and the framework class.

Equations

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

@[simp]

theorem SE.NeutralSubstrate.Neutrality.interpretiveNonCommitment_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} : InterpretiveNonCommitment C S s M ↔ ∀ (p : L.Proposition), FrameworkRelative.FrameworkVariantProposition C S s M p → ¬Substrate.SubstrateCommitment C S s p ∧ ¬Substrate.SubstrateCommitment C S s (L.neg p)

A substrate satisfies interpretive non-commitment exactly when it commits to neither a framework-variant proposition nor its object-language negation.

theorem SE.NeutralSubstrate.Neutrality.not_substrateCommitment_of_interpretiveNonCommitment {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} (hnonCommitment : InterpretiveNonCommitment C S s M) {p : L.Proposition} (hvariant : FrameworkRelative.FrameworkVariantProposition C S s M p) : ¬Substrate.SubstrateCommitment C S s p

A substrate satisfying interpretive non-commitment does not commit to a framework-variant proposition.

theorem SE.NeutralSubstrate.Neutrality.not_negSubstrateCommitment_of_interpretiveNonCommitment {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} (hnonCommitment : InterpretiveNonCommitment C S s M) {p : L.Proposition} (hvariant : FrameworkRelative.FrameworkVariantProposition C S s M p) : ¬Substrate.SubstrateCommitment C S s (L.neg p)

A substrate satisfying interpretive non-commitment does not commit to the object-language negation of a framework-variant proposition.

theorem SE.NeutralSubstrate.Neutrality.no_commitment_pair_of_interpretiveNonCommitment {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} (hnonCommitment : InterpretiveNonCommitment C S s M) {p : L.Proposition} (hvariant : FrameworkRelative.FrameworkVariantProposition C S s M p) : ¬Substrate.SubstrateCommitment C S s p ∧ ¬Substrate.SubstrateCommitment C S s (L.neg p)

Interpretive non-commitment supplies both non-commitment conclusions for a framework-variant proposition.