A relational Heyting algebra is the algebraic structure that the relationality derivation produces at step 12 (Order and Algebra), when judgements standing in relations to each other force order, meet, join, implication, and negation.
In standard mathematics, a Heyting algebra is a bounded lattice with a binary operation of relative pseudo-complementation (implication). It is the algebraic semantics of intuitionistic (constructive) logic — a logic where the law of excluded middle does not hold, and existence claims require construction. See the existing learn-heyting-algebras skill for the standard mathematical treatment.
What distinguishes the relational Heyting algebra is its origin: it is not posited as a mathematical structure or motivated by logical considerations. It is derived. The derivation reaches it through the following forced sequence:
- Terms differentiate into positions, functions, and applications (step 10).
- Terms are witnessed through Observation and assessed through Judgement (step 11).
- Judgements stand in relations: some subsume others. This forces Order — a partial ordering on judgements.
- Order forces Meet (greatest common refinement), Join (least common coarsening), Implication (logical consequence), and Negation (implying the bottom).
- The result is a Heyting algebra. It is constructive because the derivation is constructive — every structure exists because it has been derived, so existence requires construction.
The algebra constrains the term language through Soundness, Confluence, and Normalization.
The relational Heyting algebra connects the derivation to constructive logic, type theory, and topos theory in established mathematics. It provides the logical backbone for the formal structures that follow: Flow, Nucleus, Geometry, Profiles.