Implies is the residuated implication operator --- the internal hom of the Heyting algebra of relations.
Formal Signature
Implies : (Rel, Rel) → Rel
Definition
Implies(b, c) is the largest relation a such that Together(a, b) is entailed by c. It is defined by the residuation law:
Entails(Together(a, b), c) ⟺ Entails(a, Implies(b, c))
In words: a and b together entailing c is the same as a alone entailing that b implies c. This adjunction is what distinguishes a Heyting algebra from a Boolean algebra --- implication is constructive, not classical.
Implies internalizes the Entails ordering: where Entails is a judgment about relations, Implies is itself a relation.
Derivational context
Implies arises in Movement I: Logical Origination as the internalization of conditional relating. Once recognitions can be combined (Together) and compared (Entails), the question “what must hold for this combination to entail that?” has a definite answer. Implies is that answer — it turns the external comparison into an internal relation. The residuation law connecting Together, Implies, and Entails is the structural signature of the logical core. In mathematical terms this makes the structure Heyting rather than Boolean, but relationally it reflects that some matters remain genuinely indeterminate until relational activity resolves them.