Incompatibility Triangle: Locality, Totality, and Obstruction

This post follows up on the previous thread:
A local obstruction invalidates a relation
🔗 https://www.reddit.com/r/ObstructiveLogic/comments/1khkc9l/a_local_obstruction_invalidates_a_relation/

That example showed how a single non-formable term could collapse a locally conditioned relation, even when totality was assumed.

Here, I generalize the structure behind that collapse.

Let:

• P(x) be a local validity predicate (e.g. formability, non-nullity),
• R(x, y) a binary relation we wish to treat as total.

We consider three assumptions:

• Locality R(x, y) → P(x) ∧ P(y) (The relation applies only to valid terms.)
• Totality ∀x ∀y. R(x, y) (The relation is defined everywhere.)
• Obstruction ∃x. ¬P(x) (There exists at least one invalid term.)

These three lead to contradiction:

Lemma Incompatibility :
  (∀x y, R x y → P x ∧ P y) ->
  (∀x y, R x y) ->
  (∃x, ¬P x) ->
  False.

This triangle arises across domains:

• Division by zero (P(x) := x ≠ 0)
• Unsafe operations without runtime checks
• Implicit assumptions in proof assistants
• Type systems without dependent constraints