Foundational-Layer Restriction

The structural predicate shared by the neutrality constraint and the sufficiency direction: the foundational layer is restricted to the permitted classes when every substrate-layer commitment is either a referential commitment or a permitted attribution proposition.

It depends only on referential commitments and permitted attribution propositions, so stated below the constraint and the sufficiency argument that use it.

def SE.NeutralSubstrate.FoundationalLayerRestrictedToPermittedClasses {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} (C : Logic.ConsequenceSystem L) (S : Substrate.SubstrateSystem L R) (F : Substrate.ReferentialFixing L R) (A : Attribution.AttributionSystem L) (B : Attribution.AttributionalBasisFixing C A) (s : S.Carrier) : Prop

The foundational layer is restricted to the permitted classes when every substrate-layer commitment is either a referential commitment or a permitted attribution proposition. The restriction applies to semantic substrate-layer commitments. This is a theory concept, so we expose the associated _iff theorem rather than use @expose.

Equations

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

@[simp]

theorem SE.NeutralSubstrate.foundationalLayerRestrictedToPermittedClasses_iff {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {A : Attribution.AttributionSystem L} {B : Attribution.AttributionalBasisFixing C A} {s : S.Carrier} : FoundationalLayerRestrictedToPermittedClasses C S F A B s ↔ ∀ (p : L.Proposition), Substrate.SubstrateCommitment C S s p → p ∈ Substrate.ReferentialCommitments C S F s ∨ Attribution.PermittedAttributionProposition C S F A B s p

A foundational layer is restricted to the permitted classes exactly when every substrate commitment is a referential commitment or a permitted attribution proposition.