Documentation

SE.NeutralSubstrate.FrameworkRelative.Variant

Framework-Variant Propositions #

This module formalizes:

A proposition is framework-variant with respect to a substrate and the framework class when there exist two admissible frameworks such that the substrate combined with one framework entails the proposition, while the substrate combined with the other entails its object-language negation.

The two witnessing frameworks are not required to be distinct. No decidability, finiteness, enumeration, or effective search procedure for the framework class is assumed.

source
def SE.NeutralSubstrate.FrameworkRelative.SubstrateFrameworkCommitments {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} (S : Substrate.SubstrateSystem L R) (s : S.Carrier) (M : Framework.FrameworkSystem L.carrier) (framework : M.Carrier) :
Logic.Theory.CommitmentTheory L.carrier

The commitment theory obtained by combining a substrate's commitments with an interpretive framework's commitments.

This formalizes the paper's notation S ∪ F.

Equations
Instances For
    source
    @[simp]
    theorem SE.NeutralSubstrate.FrameworkRelative.substrateFrameworkCommitments_eq {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} {framework : M.Carrier} :
    SubstrateFrameworkCommitments S s M framework = Logic.Theory.combine (S.commitments s) (M.commitments framework)

    The substrate-framework commitment theory is the union of the substrate's commitments with the framework's commitments.

    source
    theorem SE.NeutralSubstrate.FrameworkRelative.entails_substrateFrameworkCommitments_of_substrateCommitment {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} {framework : M.Carrier} {p : L.Proposition} (hp : Substrate.SubstrateCommitment C S s p) :
    C.entails (SubstrateFrameworkCommitments S s M framework) p

    A substrate-layer commitment remains entailed after combining the substrate with any framework.

    source
    def SE.NeutralSubstrate.FrameworkRelative.FrameworkVariantProposition {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} (C : Logic.ConsequenceSystem L) (S : Substrate.SubstrateSystem L R) (s : S.Carrier) (M : Framework.FrameworkSystem L.carrier) (p : L.Proposition) :
    Prop

    A proposition is framework-variant with respect to a substrate and framework class when there exist admissible frameworks such that one corresponding substrate-framework theory entails the proposition and another entails its object-language negation.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem SE.NeutralSubstrate.FrameworkRelative.frameworkVariantProposition_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} {p : L.Proposition} :
      FrameworkVariantProposition C S s M p ↔ ∃ (frameworkOne : M.Carrier), ∃ (frameworkTwo : M.Carrier), frameworkOne ∈ Framework.FrameworkClass C M ∧ frameworkTwo ∈ Framework.FrameworkClass C M ∧ C.entails (SubstrateFrameworkCommitments S s M frameworkOne) p ∧ C.entails (SubstrateFrameworkCommitments S s M frameworkTwo) (L.neg p)

      A proposition is framework-variant exactly when it has two admissible framework witnesses giving the opposed entailments required by the definition.

      source
      theorem SE.NeutralSubstrate.FrameworkRelative.exists_entails_of_frameworkVariantProposition {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} {p : L.Proposition} (hp : FrameworkVariantProposition C S s M p) :
      ∃ (framework : M.Carrier), framework ∈ Framework.FrameworkClass C M ∧ C.entails (SubstrateFrameworkCommitments S s M framework) p

      A framework-variant proposition is entailed by the substrate combined with some admissible framework.

      source
      theorem SE.NeutralSubstrate.FrameworkRelative.exists_entailsNeg_of_frameworkVariantProposition {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} {p : L.Proposition} (hp : FrameworkVariantProposition C S s M p) :
      ∃ (framework : M.Carrier), framework ∈ Framework.FrameworkClass C M ∧ C.entails (SubstrateFrameworkCommitments S s M framework) (L.neg p)

      The object-language negation of a framework-variant proposition is entailed by the substrate combined with some admissible framework.