Attribution Propositions

This module formalizes:

• se100.def.AttributionProposition — Attribution Proposition

An attribution proposition is an object-language proposition of the form asserts x φ, meaning that a framework, source, agent, institution, record, or document x asserts proposition φ.

The source carrier and the proposition-forming operation are abstract. Concrete realizations may represent different kinds of attribution sources within the same carrier.

No injectivity, decidable equality, source enumeration, or computational encoding assumption is imposed.

In particular, this module introduces no entailment from asserts x φ to φ. A substrate may therefore commit to the attribution proposition without thereby committing to the asserted proposition.

structure SE.NeutralSubstrate.Attribution.AttributionSystem (L : Logic.Language.PropositionalLanguage) : Type (max u (v + 1))

An object-language attribution interface.

Source supplies the possible bearers of attributed assertions. asserts x φ is the object-language proposition stating that source x asserts proposition φ.

• Source : Type v

  The carrier of frameworks, sources, agents, institutions, records, documents, or other identified attribution sources.

• asserts : self.Source → L.Proposition → L.Proposition

  The object-language proposition stating that a source asserts a proposition.

def SE.NeutralSubstrate.Attribution.AttributionProposition {L : Logic.Language.PropositionalLanguage} (A : AttributionSystem L) (p : L.Proposition) : Prop

An attribution proposition is a proposition of the form asserts x φ for some attribution source x and asserted proposition φ.

Equations

• SE.NeutralSubstrate.Attribution.AttributionProposition A p = ∃ (x : A.Source), ∃ (φ : L.Proposition), p = A.asserts x φ

theorem SE.NeutralSubstrate.Attribution.attributionProposition_asserts {L : Logic.Language.PropositionalLanguage} (A : AttributionSystem L) (x : A.Source) (φ : L.Proposition) : AttributionProposition A (A.asserts x φ)

Every proposition constructed by asserts is an attribution proposition.

theorem SE.NeutralSubstrate.Attribution.exists_asserts_eq_of_attributionProposition {L : Logic.Language.PropositionalLanguage} {A : AttributionSystem L} {p : L.Proposition} (hp : AttributionProposition A p) : ∃ (x : A.Source), ∃ (φ : L.Proposition), p = A.asserts x φ

An attribution proposition has a source and an asserted proposition whose attribution form equals it.