The Heyting implication a → b is the largest element c such that a ∧ c ≤ b. Equivalently, it is defined by the residuation law:
c ≤ (a → b) if and only if (c ∧ a) ≤ b
This makes → the right adjoint of the meet operation ∧. For any fixed a, the functor (a ∧ −) has a right adjoint (a → −), and this adjunction is what defines the implication.
In Boolean logic, a → b reduces to ¬a ∨ b — implication is definable from negation and disjunction. In a Heyting algebra, this reduction fails. The Heyting implication carries more information than Boolean implication because it encodes the constructive content of “if a then b”: it represents the largest context in which a entails b, not just the truth value of the conditional.
Negation in a Heyting algebra is defined as ¬a = (a → ⊥), the implication from a to the bottom element. This gives intuitionistic negation: ¬¬a ≥ a always holds, but ¬¬a = a (double negation elimination) may fail. The gap between a and ¬¬a measures how far the algebra departs from classical logic.
The Heyting implication is the internal hom of the lattice viewed as a category: (a → b) is the “space of proofs” from a to b. In a topos, the Heyting implication of the subobject classifier gives the internal implication of the topos’s logic.
In the semiotic universe, the Heyting implication governs the derivation’s logical structure: each step of the forcing argument uses the fact that if a ∧ c ≤ b, there is a largest such c — the strongest additional condition compatible with the entailment.