Commitment Consistency

SE.Persistence.Commitment.Consistency

Identity judgments as constraints. A body of judgments has two parts:

• P: pairs asserted to be the same individual;
• D: pairs asserted to be distinct individuals.

An identity relation is admissible for (P, D) when it is an equivalence relation that contains every pair of P and no pair of D.

The main fact is that an admissible relation exists exactly when the equivalence relation generated by P contains no pair of D. The generated relation is the least equivalence containing P, so it is the only candidate that needs checking.

This module does not say where P or D come from. They are inputs, and a wrong input gives a wrong consequence. In particular, the identity relation of a classification is Generated of its preserving steps, so it is the P-closure for P equal to those steps.

def SE.Persistence.Admissible {C : Type} (P D E : C → C → Prop) : Prop

E is an admissible identity relation for same-commitments P and distinct-commitments D: an equivalence relation containing P and no pair of D.

Equations

• SE.Persistence.Admissible P D E = (Equivalence E ∧ (∀ (x y : C), P x y → E x y) ∧ ∀ (x y : C), D x y → ¬E x y)

def SE.Persistence.Consistent {C : Type} (P D : C → C → Prop) : Prop

P and D are consistent: no pair asserted distinct is in the equivalence relation generated by P.

Generated P is symmetric, so this also controls D y x whenever D x y.

Equations

• SE.Persistence.Consistent P D = ∀ (x y : C), D x y → ¬SE.Persistence.Generated P x y

theorem SE.Persistence.admissible_generated_of_consistent {C : Type} {P D : C → C → Prop} (h : Consistent P D) : Admissible P D (Generated P)

When the commitments are consistent, the generated relation is admissible.

theorem SE.Persistence.consistent_of_admissible {C : Type} {P D E : C → C → Prop} (h : Admissible P D E) : Consistent P D

An admissible relation makes the commitments consistent.

theorem SE.Persistence.consistent_iff_exists_admissible {C : Type} {P D : C → C → Prop} : Consistent P D ↔ ∃ (E : C → C → Prop), Admissible P D E

Consistency is exactly the existence of an admissible identity relation.

theorem SE.Persistence.Consistent.mono {C : Type} {P P' D D' : C → C → Prop} (h : Consistent P' D') (hP : ∀ (x y : C), P x y → P' x y) (hD : ∀ (x y : C), D x y → D' x y) : Consistent P D

Consistency is monotone downward: fewer commitments stay consistent.

theorem SE.Persistence.consistent_union_iff {C : Type} {P D₁ D₂ : C → C → Prop} : (Consistent P fun (x y : C) => D₁ x y ∨ D₂ x y) ↔ Consistent P D₁ ∧ Consistent P D₂

Distinctness from two independent sources is consistent with P exactly when each source is. Several observers can be checked one at a time.

Witnesses

A generated identity has a finite explanation: a chain of asserted pairs, each used in either direction.

def SE.Persistence.SymmStep {C : Type} (r : C → C → Prop) : C → C → Prop

One asserted pair of r, used in either direction.

Equations

• SE.Persistence.SymmStep r x y = (r x y ∨ r y x)

theorem SE.Persistence.Reach.symm_of_symmetric {C : Type} {s : C → C → Prop} (hs : ∀ (x y : C), s x y → s y x) {x y : C} (h : Reach s x y) : Reach s y x

Reach along a symmetric step relation can be reversed.

theorem SE.Persistence.Generated.of_reach_symmStep {C : Type} {r : C → C → Prop} {x y : C} (h : Reach (SymmStep r) x y) : Generated r x y

A chain of asserted pairs gives a generated identity.

theorem SE.Persistence.Generated.to_reach_symmStep {C : Type} {r : C → C → Prop} {x y : C} (h : Generated r x y) : Reach (SymmStep r) x y

A generated identity gives a chain of asserted pairs.

theorem SE.Persistence.generated_iff_reach_symmStep {C : Type} {r : C → C → Prop} {x y : C} : Generated r x y ↔ Reach (SymmStep r) x y

x and y are generated-identical exactly when a finite chain of asserted pairs, each used in either direction, connects them. The chain is the explanation for the identity.