# Object-Level Interpretive Propositions

This module formalizes:

• se100.def.ObjectLevelInterpretiveProposition - Object-Level Interpretive Proposition

An object-level interpretive proposition is an object-language proposition whose subject matter concerns the referential domain governed by a substrate's referential regime, rather than an attribution proposition stating that some source asserts it.

The relationship between proposition content and a referential regime is represented abstractly. This module does not define a denotation relation from proposition content or references to particular referent-carrier elements.

Being non-attributional is not sufficient. An object-level interpretive proposition must also concern the referential subject matter governed by the substrate's referential regime.

In particular, aboutReferents does not by itself establish:

• denotation of a particular carrier element;
• co-reference;
• same-unit identity;
• persistence;
• carrier equality; or
• referential fixing of the proposition.

No decidability, exhaustiveness, syntactic decomposition, denotation procedure, or computational classification assumption is imposed.

structure SE.NeutralSubstrate.Interpretation.ObjectLevelInterpretation (L : Logic.Language.PropositionalLanguage) (R : Referent.ReferentCarriers) : Type (max u (v + 1))

An abstract account of whether an object-language proposition concerns the referential subject matter governed by a referential regime.

Concrete realizations may determine this relation through a typed object-language, declared proposition roles, semantic interpretation, or another fixed accountability-context method.

This interface classifies proposition subject matter. It does not supply the deferred denotation or co-reference lifting bridges and does not identify aboutness with referential fixing.

• aboutReferents : Substrate.ReferentialRegime R → L.Proposition → Prop

  Whether a proposition concerns the referential subject matter governed by a referential regime.

def SE.NeutralSubstrate.Interpretation.ObjectLevelInterpretiveProposition {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} (A : Attribution.AttributionSystem L) (I : ObjectLevelInterpretation L R) (S : Substrate.SubstrateSystem L R) (s : S.Carrier) (p : L.Proposition) : Prop

A proposition is object-level interpretive relative to a substrate when:

1. it concerns the referential subject matter governed by that substrate's referential regime; and
2. it is not an attribution proposition.

The definition classifies the proposition. It does not state that the substrate commits to that proposition or that the proposition denotes any particular referent-carrier element.

Equations

• SE.NeutralSubstrate.Interpretation.ObjectLevelInterpretiveProposition A I S s p = (I.aboutReferents (S.referentialRegime s) p ∧ ¬SE.NeutralSubstrate.Attribution.AttributionProposition A p)

@[simp]

theorem SE.NeutralSubstrate.Interpretation.objectLevelInterpretiveProposition_iff {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {A : Attribution.AttributionSystem L} {I : ObjectLevelInterpretation L R} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} {p : L.Proposition} : ObjectLevelInterpretiveProposition A I S s p ↔ I.aboutReferents (S.referentialRegime s) p ∧ ¬Attribution.AttributionProposition A p

A proposition is object-level interpretive exactly when it concerns the referential subject matter governed by the substrate's referential regime and is not an attribution proposition.

theorem SE.NeutralSubstrate.Interpretation.aboutReferents_of_objectLevelInterpretiveProposition {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {A : Attribution.AttributionSystem L} {I : ObjectLevelInterpretation L R} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} {p : L.Proposition} (hp : ObjectLevelInterpretiveProposition A I S s p) : I.aboutReferents (S.referentialRegime s) p

Every object-level interpretive proposition concerns the referential subject matter governed by the substrate's referential regime.

theorem SE.NeutralSubstrate.Interpretation.not_attributionProposition_of_objectLevelInterpretiveProposition {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {A : Attribution.AttributionSystem L} {I : ObjectLevelInterpretation L R} {S : Substrate.SubstrateSystem L R} {s : S.Carrier} {p : L.Proposition} (hp : ObjectLevelInterpretiveProposition A I S s p) : ¬Attribution.AttributionProposition A p

No object-level interpretive proposition is an attribution proposition under the selected attribution system.