Contextual Commitments

SE.Coreference.ContextualCommitments

Reads a co-reference account through the Persistence commitment calculus, one context at a time.

In a context c, the account's coReference c is read as the asserted-same pairs P. Distinct-commitments D are a separate input. They are not derived from the failure of coReference: a pair that is not co-referent is not thereby established to refer to different wholes.

The equivalence closure of coReference c can establish pairs the account does not. It is therefore named separately, and it coincides with coReference c only under hypotheses such as Equivalence (coReference c). When closure is warranted is not settled here.

Persistence states its calculus for carriers in Type, so this module specializes the account to universe 0, as Individuation does.

structure SE.Coreference.DistinctCommitments {Referent : Type} (A : Substrate.CoReferenceAccount Referent) : Type

Independently warranted distinct-commitments in each context of an account.

• distinct : A.Context → A.Reference → A.Reference → Prop

  distinct c x y: x and y are asserted to refer to different wholes in context c.

def SE.Coreference.GeneratedCoReference {Referent : Type} (A : Substrate.CoReferenceAccount Referent) (c : A.Context) (x y : A.Reference) : Prop

Two references are generated co-referent in a context when the equivalence closure of the account's co-reference links them.

Equations

• SE.Coreference.GeneratedCoReference A c x y = SE.Persistence.Generated (A.coReference c) x y

def SE.Coreference.ContextConsistent {Referent : Type} (A : Substrate.CoReferenceAccount Referent) (D : DistinctCommitments A) (c : A.Context) : Prop

In a context, the account's co-reference and the distinct-commitments are consistent in the sense of Persistence.

Equations

• SE.Coreference.ContextConsistent A D c = SE.Persistence.Consistent (A.coReference c) (D.distinct c)

theorem SE.Coreference.coReference_imp_generatedCoReference {Referent : Type} (A : Substrate.CoReferenceAccount Referent) (c : A.Context) {x y : A.Reference} (h : A.coReference c x y) : GeneratedCoReference A c x y

Whatever the account judges co-referent in a context is generated co-referent.

theorem SE.Coreference.generatedCoReference_iff_of_equivalence {Referent : Type} (A : Substrate.CoReferenceAccount Referent) (c : A.Context) (hEq : Equivalence (A.coReference c)) {x y : A.Reference} : GeneratedCoReference A c x y ↔ A.coReference c x y

When the account's co-reference in a context is already an equivalence relation, closure adds no pairs.

theorem SE.Coreference.contextConsistent_iff_exists_admissible {Referent : Type} (A : Substrate.CoReferenceAccount Referent) (D : DistinctCommitments A) (c : A.Context) : ContextConsistent A D c ↔ ∃ (E : A.Reference → A.Reference → Prop), Persistence.Admissible (A.coReference c) (D.distinct c) E

In a context, the commitments are consistent exactly when some admissible identity relation exists.

theorem SE.Coreference.undetermined_of_not_generatedCoReference_of_no_distinct {Referent : Type} (A : Substrate.CoReferenceAccount Referent) (c : A.Context) {x y : A.Reference} (h : ¬GeneratedCoReference A c x y) : Persistence.Undetermined (A.coReference c) (fun (x x_1 : A.Reference) => False) x y

With no distinct-commitments, a pair that is not generated co-referent is undetermined, not distinct.