Commitment Status

SE.Persistence.Commitment.Status

What consistent commitments (P, D) say about a further pair (x, y):

• Required: x and y are identical in every admissible identity relation;
• Forbidden: x and y are distinct in every admissible identity relation;
• Undetermined: some admissible relation identifies them and some separates them.

The definitions are syntactic, and the theorems show they coincide with the semantic readings above. A new distinction can therefore be forced although nobody asserted it: if a and b are identical and a and c are distinct, then b and c are forbidden to be identical.

This calculus uses equivalence laws only. It assumes no limit on the number of individuals. SE.Persistence.Commitment.Interpretation adds extra constraints, such as a class limit from SE.Persistence.Commitment.Cardinality.

def SE.Persistence.Extend {C : Type} (P : C → C → Prop) (a b : C) : C → C → Prop

P together with one further asserted pair (a, b).

Equations

• SE.Persistence.Extend P a b x y = (P x y ∨ x = a ∧ y = b)

def SE.Persistence.Required {C : Type} (P : C → C → Prop) (x y : C) : Prop

x and y are required to be identical: they are generated-identical.

Equations

• SE.Persistence.Required P x y = SE.Persistence.Generated P x y

def SE.Persistence.Forbidden {C : Type} (P D : C → C → Prop) (x y : C) : Prop

x and y are forbidden to be identical: asserting them identical would generate identity between some pair asserted distinct.

Equations

• SE.Persistence.Forbidden P D x y = ∃ (u : C), ∃ (v : C), D u v ∧ SE.Persistence.Generated (SE.Persistence.Extend P x y) u v

def SE.Persistence.Undetermined {C : Type} (P D : C → C → Prop) (x y : C) : Prop

Neither required nor forbidden.

Equations

• SE.Persistence.Undetermined P D x y = (¬SE.Persistence.Required P x y ∧ ¬SE.Persistence.Forbidden P D x y)

theorem SE.Persistence.generated_extend_self {C : Type} (P : C → C → Prop) (a b : C) : Generated (Extend P a b) a b

Extending by a pair makes that pair generated-identical.

theorem SE.Persistence.generated_extend_of_generated {C : Type} {P : C → C → Prop} {a b x y : C} (h : Generated P x y) : Generated (Extend P a b) x y

Extending keeps every earlier asserted pair.

theorem SE.Persistence.generated_extend_le {C : Type} {P D E : C → C → Prop} {a b : C} (hE : Admissible P D E) (hab : E a b) {x y : C} (h : Generated (Extend P a b) x y) : E x y

An admissible relation that identifies a and b contains the extension.

theorem SE.Persistence.required_iff_forall_admissible {C : Type} {P D : C → C → Prop} (hc : Consistent P D) {x y : C} : Required P x y ↔ ∀ (E : C → C → Prop), Admissible P D E → E x y

Under consistent commitments, a pair is required exactly when every admissible identity relation identifies it.

theorem SE.Persistence.forbidden_iff_forall_admissible {C : Type} {P D : C → C → Prop} {x y : C} : Forbidden P D x y ↔ ∀ (E : C → C → Prop), Admissible P D E → ¬E x y

A pair is forbidden exactly when every admissible identity relation separates it. This holds without assuming the commitments are consistent: if none is, both sides are true.

theorem SE.Persistence.undetermined_iff {C : Type} {P D : C → C → Prop} (hc : Consistent P D) {x y : C} : Undetermined P D x y ↔ (∃ (E : C → C → Prop), Admissible P D E ∧ E x y) ∧ ∃ (E : C → C → Prop), Admissible P D E ∧ ¬E x y

Under consistent commitments, a pair is undetermined exactly when one admissible relation identifies it and another separates it.

theorem SE.Persistence.not_required_and_forbidden {C : Type} {P D : C → C → Prop} (hc : Consistent P D) {x y : C} : ¬(Required P x y ∧ Forbidden P D x y)

Under consistent commitments, no pair is both required and forbidden.

theorem SE.Persistence.required_mono {C : Type} {P P' : C → C → Prop} (h : ∀ (x y : C), P x y → P' x y) {x y : C} (hr : Required P x y) : Required P' x y

Adding same-commitments keeps every requirement.

theorem SE.Persistence.forbidden_mono {C : Type} {P P' D D' : C → C → Prop} (hP : ∀ (x y : C), P x y → P' x y) (hD : ∀ (x y : C), D x y → D' x y) {x y : C} (hf : Forbidden P D x y) : Forbidden P' D' x y

Adding same-commitments or distinct-commitments keeps every prohibition. Statuses only resolve as commitments grow, until the commitments become inconsistent.

theorem SE.Persistence.forbidden_of_distinct {C : Type} {P D : C → C → Prop} {x y : C} (h : D x y) : Forbidden P D x y

A pair asserted distinct is forbidden to be identical.

theorem SE.Persistence.forbidden_of_required_of_distinct {C : Type} {P D : C → C → Prop} {a b c : C} (hab : Required P a b) (hac : D a c) : Forbidden P D b c

A forced distinction. If a and b are required identical and a and c are asserted distinct, then b and c are forbidden to be identical, though no one asserted it.