Substrate-Layer Commitment #
This module formalizes:
se100.def.SubstrateCommitment— Substrate-Layer Commitment
A substrate commits to an object-language proposition when that proposition is entailed by the substrate's commitment theory independently of any interpretive framework.
This definition does not classify the proposition as referential, attributional, interpretive, causal, or normative. Those classifications are defined separately.
def
SE.Substrate.SubstrateCommitment
{L : Logic.Language.PropositionalLanguage}
{R : Referent.ReferentCarriers}
(C : Logic.ConsequenceSystem L)
(S : SubstrateSystem L R)
(s : S.Carrier)
(p : L.Proposition)
:
A substrate-layer commitment to p holds exactly when the substrate's
commitment theory entails p.
Equations
- SE.Substrate.SubstrateCommitment C S s p = C.entails (S.commitments s) p
Instances For
theorem
SE.Substrate.entails_of_substrateCommitment
{L : Logic.Language.PropositionalLanguage}
{R : Referent.ReferentCarriers}
{C : Logic.ConsequenceSystem L}
{S : SubstrateSystem L R}
{s : S.Carrier}
{p : L.Proposition}
(hp : SubstrateCommitment C S s p)
:
C.entails (S.commitments s) p
A substrate-layer commitment entails the committed proposition from the substrate's commitment theory.
theorem
SE.Substrate.substrateCommitment_of_entails
{L : Logic.Language.PropositionalLanguage}
{R : Referent.ReferentCarriers}
{C : Logic.ConsequenceSystem L}
{S : SubstrateSystem L R}
{s : S.Carrier}
{p : L.Proposition}
(hp : C.entails (S.commitments s) p)
:
SubstrateCommitment C S s p
Entailment from a substrate's commitment theory establishes a substrate-layer commitment.