Substrate Consistency

This module formalizes:

• se100.assump.SubstrateConsistency — Substrate Consistency

Every substrate considered by the theory is internally consistent. Its commitment theory does not entail contradiction:

S ⊬ ⊥.

Substrate consistency concerns the substrate in isolation. It is distinct from extension stability, which requires consistency after combining the substrate with every admissible framework.

No decidability or effective consistency-checking procedure is assumed.

def SE.NeutralSubstrate.Assumptions.SubstrateConsistency {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} (C : Logic.ConsequenceSystem L) (S : Substrate.SubstrateSystem L R) (s : S.Carrier) : Prop

A substrate is internally consistent when its commitment theory does not entail the object-language contradiction.

This formalizes the paper's condition:

S ⊬ ⊥.

Equations

• SE.NeutralSubstrate.Assumptions.SubstrateConsistency C S s = SE.Logic.Consistent C (S.commitments s)

@[simp]

theorem SE.NeutralSubstrate.Assumptions.substrateConsistency_iff {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} : SubstrateConsistency C S s ↔ Logic.Consistent C (S.commitments s)

A substrate is consistent exactly when its commitment theory is consistent.

theorem SE.NeutralSubstrate.Assumptions.consistent_of_substrateConsistency {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} (hconsistency : SubstrateConsistency C S s) : Logic.Consistent C (S.commitments s)

Substrate consistency supplies consistency of the substrate's commitment theory.

theorem SE.NeutralSubstrate.Assumptions.substrateConsistency_of_consistent {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} (hconsistency : Logic.Consistent C (S.commitments s)) : SubstrateConsistency C S s

Consistency of the substrate's commitment theory establishes substrate consistency.