What this lesson covers
How the relationality derivation produces a Heyting algebra — the algebraic structure of constructive logic — from the relations among judgements. By the end, you will understand what a Heyting algebra is, why the derivation produces one rather than a Boolean algebra, and what this means for the formal structures that follow.
Why it matters
The Heyting algebra at step 12 is the bridge between the derivation’s philosophical content (relational coherence, boundary, reflexion, field) and its mathematical content (terms, types, dynamics, geometry). The algebra gives the derivation a logic — not classical logic, but constructive logic. Understanding why the logic is constructive, and what that means, is essential for understanding the formal structures that build on it.
Prerequisites
- Terms and Logic from the derivation curriculum — you need to understand how terms, observation, judgement, and order arise in the derivation.
- Familiarity with the idea of a partial order (some things are “below” or “above” others, but not all pairs are comparable). If this is unfamiliar, see the existing learn-about-order-theory skill.
Core concepts
What a Heyting algebra is
Imagine a collection of questions that can be asked about a system. Some questions are more specific than others: “Is this an oak tree?” is more specific than “Is this a tree?” If question A is more specific than question B, we write A ≤ B (A refines B).
This ordering has natural operations:
- Meet (A ∧ B): the most specific question that both A and B agree on. “Is this a deciduous oak?” meets “Is this an oak in North America?” at something like “Is this a deciduous oak in North America?”
- Join (A ∨ B): the least specific question that captures both A and B. The join of “Is this an oak?” and “Is this a maple?” is something like “Is this a hardwood?”
- Implication (A → B): the weakest question C such that C together with A is at least as specific as B. In other words: “what would you need to add to A to get B?”
A Heyting algebra is a structure with these operations — order, meet, join, and implication — satisfying certain laws. The critical feature: implication is defined relative to meet, through what mathematicians call residuation. The implication A → B is the greatest C such that C ∧ A ≤ B.
For the standard mathematical treatment, see Heyting algebras in mathematics and the learn-heyting-algebras skill.
Why constructive, not classical?
A Boolean algebra is a Heyting algebra where an additional law holds: for every proposition A, either A or its negation is true (the law of excluded middle). Classical logic is Boolean.
The derivation does not produce a Boolean algebra. Why? Because the law of excluded middle requires that every question has a definite yes-or-no answer, even without construction. But in the derivation, nothing exists without having been derived. You cannot assert “this or not-this” unless you can construct which one holds.
Think of it this way: in the derivation, to say “X exists” means “X has been derived — here is the construction.” To say “X or not-X” would require either producing X or producing a proof that X is impossible. The derivation cannot shortcut this by assuming one or the other holds.
This is not a limitation — it is a feature. Constructive logic carries more information than classical logic. A constructive proof of “there exists an X” always comes with a witness: the X itself.
How the derivation produces it
The forcing sequence at step 12:
- Judgements (from step 11) stand in relations to each other.
- Those relations force Order: some judgements subsume others. This is a partial order — not all pairs of judgements are comparable.
- Order forces Meet: given two judgements, what is their greatest common refinement?
- Order forces Join: given two judgements, what is their least common coarsening?
- Meet and join together make a lattice. But a lattice alone does not have logical structure.
- The lattice forces Implication: given two judgements, what is the greatest judgement whose meet with the first is below the second? This is residuation applied to judgements.
- Implication forces Negation: the implication of a judgement to the bottom (the trivially empty judgement). Negation is “implies absurdity.”
The result is a Heyting algebra. Each operation is forced by the structural requirements of what came before.
What the algebra does to the syntax
The Heyting algebra is not just a logic — it constrains the term language from step 10:
- Soundness: well-typed terms do not go wrong. If a term has been assigned a type (a judgement about what it is), evaluating that term will not produce nonsense.
- Confluence: different reduction paths reach the same result. The order in which you simplify does not matter.
- Normalization: every term reaches a value. Simplification always terminates.
These are the Curry-Howard correspondence made concrete: the algebra (logic) and the term language (computation) are two sides of the same structure.
Worked example
Trace implication as residuation:
Suppose you have three judgements: A = “this is a tree,” B = “this is an oak,” and C = “this tree is in North America.”
- B ≤ A (being an oak refines being a tree).
- The implication A → B asks: what is the greatest judgement C such that C ∧ A ≤ B? That is: what additional information, together with “this is a tree,” would refine to “this is an oak”? The answer is something like “this is of the genus Quercus” — the minimal information that bridges the gap from A to B.
- This is residuation: implication is the right adjoint to meet.
Check your understanding
1. What is the key structural difference between a [Heyting](../../../../../../general/people/arend-heyting.md) algebra and a [Boolean algebra](../../../../../../mathematics/concepts/boolean-algebra/index.md)?
In a Boolean algebra, every element has a complement (the law of excluded middle holds: A ∨ ¬A = top for all A). In a Heyting algebra, this does not necessarily hold. Negation exists (as implication to the bottom), but A ∨ ¬A may not equal the top element.
2. Why does the derivation produce constructive logic rather than classical logic?
Because nothing in the derivation exists without construction. Asserting “A or not-A” without being able to construct which one holds would require an assumption the derivation has not made. The logic that emerges from “existence requires derivation” is constructive.
3. What is residuation in the context of the [Heyting](../../../../../../general/people/arend-heyting.md) algebra?
Residuation is the relationship between meet and implication: the implication A → B is the greatest C such that C ∧ A ≤ B. Meet and implication are adjoint operations — each determines the other.
4. What does soundness guarantee about the term language?
Soundness guarantees that well-typed terms do not go wrong — if a term has been assigned a type through the judgement system, evaluating it produces a well-defined result, not nonsense.
Common mistakes
- Treating the Heyting algebra as “weaker” than Boolean. Constructive logic is not a deficiency. It carries more information (existence claims come with witnesses) and applies in more settings (toposes, computation, the derivation itself).
- Confusing residuation with subtraction. Residuation is not “A minus B.” It is the greatest thing you can combine with A (via meet) while staying below B. The direction matters.
- Thinking the algebra is imposed on the derivation. The derivation does not assume a Heyting algebra and work with it. It derives the Heyting algebra from the relations among judgements. The algebra is a consequence, not a premise.
What comes next
The Heyting algebra provides the logical backbone for everything that follows in the derivation: stability, flow, nucleus, geometry, profiles. The concept of Residuation in the Derivation traces how the same adjunction pattern recurs at three levels: logic (implication/meet), dynamics (flow/nucleus), and physics (evolution/measurement).