A local obstruction invalidates a relation.

This short Coq fragment illustrates how a local obstruction can prevent the instantiation of a relation — without requiring any form of global quantification.

It shows that formability (`Id`) can be a structural prerequisite for applying a relation such as `le_rel`. When this condition is not satisfied, even a pointwise application like `le_rel e e` can lead to contradiction.

In systems where totality is often implicit in the design of relations, this kind of local constraint highlights how formal reasoning may behave near its definitional boundaries.

We assume:

- A type `T`

- A formability predicate `Id : T -> Prop`

- A relation `le_rel : T -> T -> Prop`, which is only meant to apply to `Id`-valid terms

Then we construct:

Section PointwiseObstruction.

Variable T : Type.

Variable Id : T -> Prop.

Variable le_rel : T -> T -> Prop.

(* Structural assumption: le_rel e e implies e satisfies Id *)

Variable e : T.

Hypothesis le_rel_requires_Id : le_rel e e -> Id e /\ Id e.

(* Suppose e is obstructed *)

Hypothesis obstructed : ~ Id e.

(* Attempting to apply the relation *)

Definition absurd_totality_attempt : Prop := le_rel e e.

(* Leads to contradiction *)

Theorem pointwise_obstruction : absurd_totality_attempt -> False.

Proof.

intro H.

apply le_rel_requires_Id in H as [Hid _].

apply obstructed in Hid.

exact Hid.

Qed.

End PointwiseObstruction.

This construction does not generalize over T or over all elements. It focuses on a single term e, and shows that even minimal attempts to apply le_rel fail when e is not formable.

The system permits le_rel e e by type, but not by structure.

This opens space for reflection on how often total relations are assumed, and whether formal languages should treat formability as a first-class condition.