Documentation

SE.NeutralSubstrate.FrameworkRelative.CompatibleCommitmentSet

Framework-Compatible Commitment Sets #

This module formalizes:

A commitment set is framework-compatible when its union with the commitment theory of every admissible framework remains consistent.

Compatibility is required for the commitment set as a whole, not merely for each of its members considered separately. Individually compatible propositions may therefore fail to form a jointly compatible commitment set.

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

source
def SE.NeutralSubstrate.FrameworkRelative.FrameworkCompatibleCommitmentSet {L : Logic.Language.PropositionalLanguage} (C : Logic.ConsequenceSystem L) (M : Framework.FrameworkSystem L.carrier) (T : Logic.Theory.CommitmentTheory L.carrier) :
Prop

A commitment set is framework-compatible when combining it with every admissible framework's commitment theory produces a consistent theory.

This formalizes the paper's condition:

T ∪ F ⊬ ⊥

for every admissible framework F.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem SE.NeutralSubstrate.FrameworkRelative.frameworkCompatibleCommitmentSet_iff {L : Logic.Language.PropositionalLanguage} {C : Logic.ConsequenceSystem L} {M : Framework.FrameworkSystem L.carrier} {T : Logic.Theory.CommitmentTheory L.carrier} :
    FrameworkCompatibleCommitmentSet C M T ↔ ∀ (framework : M.Carrier), framework ∈ Framework.FrameworkClass C M → Logic.Consistent C (Logic.Theory.combine T (M.commitments framework))

    A commitment set is framework-compatible exactly when its union with every admissible framework's commitment theory remains consistent.

    source
    theorem SE.NeutralSubstrate.FrameworkRelative.consistent_combine_of_frameworkCompatibleCommitmentSet {L : Logic.Language.PropositionalLanguage} {C : Logic.ConsequenceSystem L} {M : Framework.FrameworkSystem L.carrier} {T : Logic.Theory.CommitmentTheory L.carrier} (hT : FrameworkCompatibleCommitmentSet C M T) {framework : M.Carrier} (hframework : framework ∈ Framework.FrameworkClass C M) :
    Logic.Consistent C (Logic.Theory.combine T (M.commitments framework))

    A framework-compatible commitment set remains consistent when combined with the commitments of any selected admissible framework.