Framework-Invariant Propositions

This module formalizes:

• se100.def.FrameworkInvariant — Framework-Invariant Proposition

A proposition is framework-invariant with respect to a substrate and the framework class when it can be adjoined to the substrate together with every admissible framework without producing contradiction.

The canonical formal condition is consistency after adjoining the proposition:

S ∪ F ∪ {p} ⊬ ⊥

for every admissible framework F.

The paper informally describes this as saying that no admissible framework refutes p on the shared base. This module does not identify that gloss with non-entailment of ¬p, because the abstract consequence system does not assume a negation-introduction principle.

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

def SE.NeutralSubstrate.FrameworkRelative.FrameworkInvariantProposition {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-invariant with respect to a substrate and framework class when adjoining it to every admissible substrate-framework commitment theory remains consistent.

Equations

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

@[simp]

theorem SE.NeutralSubstrate.FrameworkRelative.frameworkInvariantProposition_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} : FrameworkInvariantProposition C S s M p ↔ ∀ (framework : M.Carrier), framework ∈ Framework.FrameworkClass C M → Logic.Consistent C (Logic.Theory.adjoin (SubstrateFrameworkCommitments S s M framework) p)

A proposition is framework-invariant exactly when adjoining it to every admissible substrate-framework commitment theory remains consistent.

theorem SE.NeutralSubstrate.FrameworkRelative.consistent_adjoin_of_frameworkInvariantProposition {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 : FrameworkInvariantProposition C S s M p) {framework : M.Carrier} (hframework : framework ∈ Framework.FrameworkClass C M) : Logic.Consistent C (Logic.Theory.adjoin (SubstrateFrameworkCommitments S s M framework) p)

Adjoining a framework-invariant proposition to the substrate together with any admissible framework produces a consistent commitment theory.