Framework Invariance and Refutation #
This module formalizes:
se100.def.FrameworkInvariant- Framework-Invariant Propositionse100.remark.FrameworkInvariantRefutation- Framework Invariance and Refutation
The remark relates framework invariance to the refutation gloss
"no admissible framework refutes p on the shared base".
Refutation is read as entailment of the object-language negation neg p.
- Framework invariance implies non-refutation using the existing consequence
interface:
entailsOfMem, monotonicity, and contradiction formation. - Non-refutation implies invariance only under negation introduction:
if
adjoin T qentailsbottom, thenTentailsneg q. ConsequenceSystemdoes not assume this principle, so it is supplied as a hypothesis rather than added as a structure field.
theorem
SE.NeutralSubstrate.FrameworkRelative.not_entails_neg_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)
:
¬C.entails (SubstrateFrameworkCommitments S s M framework) (L.neg p)
A framework-invariant proposition is not refuted on any admissible
substrate-framework base: no such base entails neg p.
Proof idea: if the base entailed neg p, adjoining p would produce a theory
entailing both p and neg p, hence bottom, contradicting framework
invariance.
theorem
SE.NeutralSubstrate.FrameworkRelative.frameworkInvariantProposition_iff_not_entails_neg
{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}
(hni :
∀ {T : Logic.Theory.CommitmentTheory L.carrier} {q : L.Proposition},
C.entails (Logic.Theory.adjoin T q) L.bottom → C.entails T (L.neg q))
:
FrameworkInvariantProposition C S s M p ↔ ∀ (framework : M.Carrier),
framework ∈ Framework.FrameworkClass C M → ¬C.entails (SubstrateFrameworkCommitments S s M framework) (L.neg p)
Under the stated negation-introduction principle, framework invariance is
equivalent to non-refutation: no admissible substrate-framework base entails
neg p.
Negation introduction is a hypothesis of this theorem, not part of
ConsequenceSystem.