🔢 mathematics

Relational Semantics for Flat Heyting-Lewis Logic

This paper introduces relational semantics for "flat Heyting-Lewis logic" (HLC-flat), a variant of intuitionistic logic extended with a strict implication modality that preserves meets in its first argument, and establishes its completeness and finite model property along with those of several axiom extensions.

Original authors: Jim de Groot, Tadeusz Litak

Published 2026-07-01

📖 6 min read🧠 Deep dive

CC BY 4.0

Original authors: Jim de Groot, Tadeusz Litak

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

The Big Picture: Building a New Map for Logic

Imagine you are an architect trying to draw a map of a very strange city. This city is built on Intuitionistic Logic, which is like a city where you can't assume that every street either exists or doesn't exist until you have actually walked down it and seen it. You need proof to know a street is there.

Now, imagine you want to add a special feature to this city: a "Strict Implication" bridge. This bridge represents a very strong promise: "If you are at point A, you are guaranteed to end up at point B, no matter what." In the world of this paper, this bridge is called J.

For a long time, logicians had two ways to draw maps for this city:

The "Sharp" Map: This map is very rigid. It has a rule that says if you can get to a destination from two different starting points, you can also get there from the combination of those two points. It's like saying, "If I can walk to the park from my house, and I can walk to the park from my office, then I can walk to the park from 'my house OR my office'."
The "Flat" Map (The New Discovery): The authors of this paper are studying a version of the city where that rigid rule doesn't apply. In this "Flat" world, combining two starting points doesn't automatically guarantee you can reach the destination. This is called Flat Heyting-Lewis Logic (HLC♭).

The Problem: Logicians already had a perfect way to draw maps (semantics) for the "Sharp" version. But for the "Flat" version, they were stuck. They could describe the rules using algebra (like equations), but they couldn't find a simple, visual "Kripke-style" map (a set of dots and arrows) that worked. It was like having the blueprints for a building but no way to visualize the rooms.

The Solution: This paper finally draws the missing map. The authors, Jim de Groot and Tadeusz Litak, created a new way to visualize this "Flat" logic using a specific type of map that allows for some flexibility.

Key Concepts Explained with Analogies

1. The "Flat" vs. "Sharp" Difference

Think of the Sharp logic as a strict bouncer at a club. If you have a ticket from Person A, you get in. If you have a ticket from Person B, you get in. The Sharp rule says: "If you have a ticket from A or a ticket from B, you definitely get in."

The Flat logic is a more relaxed bouncer.

If you have a ticket from A, you get in.
If you have a ticket from B, you get in.
BUT, if you say "I have a ticket from A or B," the bouncer might say, "I don't know which one you actually have, so I can't let you in yet."
The paper shows how to draw a map where this "I don't know yet" state is perfectly valid and logical.

2. The New Map: Preorders and "Upward-Flat" Frames

To draw this map, the authors used two types of connections between dots (worlds):

The Intuitionistic Path (⪯): This is like a "knowledge" path. If you are at dot A and can reach dot B, it means you know everything A knows, plus maybe more. In the old "Sharp" maps, this path was a strict ladder (you can only go up). In this new "Flat" map, the path is a preorder. Think of it like a social network where you can be "friends with" someone, and they are "friends with" you, even if you aren't exactly the same person. It's a bit more fluid.
The Strict Bridge (R): This is the J bridge. It connects worlds where a strict promise holds.

The authors discovered that for the "Flat" logic to work, the map needs to be "Upward-Flat."

Analogy: Imagine the "Strict Bridge" (R) is a conveyor belt. In the old maps, if you stepped on the belt at point A, you could only go to specific points. In the new map, if you step on the belt at A, and the belt moves you to B, and B is "higher" (more knowledgeable) than C, then stepping on the belt at A should also let you reach C. The bridge respects the flow of knowledge.

3. Why This Matters (The "Why" of the Paper)

The authors explain that the "Sharp" rule (where combining inputs always works) is too restrictive for real-world applications in computer science and math.

Computer Science: In programming languages like Haskell, there are tools called "arrows" used to build complex software. Some of these arrows are very flexible and don't follow the "Sharp" rule. The "Flat" logic is the perfect mathematical description for these flexible tools.
Math: When studying how mathematical theories relate to each other (like Peano Arithmetic), the "Sharp" rule sometimes breaks down. The "Flat" logic handles these tricky cases better.

4. The "Canonical Model" (The Master Blueprint)

To prove their new map works, the authors built a "Canonical Model."

Analogy: Imagine you have a list of all the rules of a game. You want to prove that if a rule isn't on the list, there is a specific game scenario where that rule fails.
The authors created a "Master Game" built out of all possible logical theories. They showed that in this Master Game, their new map works perfectly. If a rule is true in the Master Game, it's true everywhere. If it's false, they can find a specific spot in the map where it breaks.
This proves two big things:
1. Completeness: The map covers all the rules of the Flat logic.
2. Finite Model Property: You don't need an infinite map to test these rules; a small, finite map is enough. This is great for computers because it means we can write software to check if these logical statements are true or false.

5. Extension Stability (The "Sub-Map" Test)

The paper ends by testing if these maps are "stable."

Analogy: Imagine you have a large city map. If you zoom in on just one neighborhood (a sub-map), do the rules still hold?
They found that the "Sharp" logic fails this test. If you zoom in on a specific neighborhood of the Sharp map, the strict rules might break.
However, the "Flat" logic (specifically with certain rules added) passes this test. This means the Flat logic is more robust and reliable when you look at smaller, specific parts of the system.

Summary

This paper is a breakthrough in the "architecture" of logic. The authors finally built a clear, visual map (relational semantics) for a flexible, "Flat" version of logic that had been elusive for years. They proved that this map is solid, works for computers (finite model property), and is more flexible than the old "Sharp" maps, making it better suited for describing complex computer programs and mathematical theories.

Technical Summary: Relational Semantics for Flat Heyting-Lewis Logic

Problem Statement
The paper addresses a gap in the semantic understanding of "flat" Heyting-Lewis logic ( $HLC^\flat$ ). While the "sharp" variant ( $HLC^\sharp$ ), which includes the axiom $(p \to r) \land (q \to r) \to ((p \lor q) \to r)$ , admits a well-established Kripke-style relational semantics, the flat system lacks a comparable simple relational interpretation. Previous attempts to model $HLC^\flat$ relied on algebraic semantics, Routley-Meyer semantics for substructural logics, or adaptations of Chellas-Weiss and Veltman semantics. The authors note that the flat system is crucial for various applications, including the Curry-Howard correspondence for arrows in functional programming (specifically those without choice), schematic logics of arithmetical theories (where sharpness fails), and intuitionistic epistemic logic. The absence of a direct Kripke-style semantics for the flat base calculus hindered the derivation of standard metatheoretic results like completeness and the finite model property (FMP) in a relational setting.

Methodology
The authors introduce a new relational semantics for $HLC^\flat$ based on flat frames, defined as tuples $(W, \preceq, R)$ where $W$ is a set of worlds, $\preceq$ is a preorder (rather than a partial order), and $R$ is a binary accessibility relation.

Semantic Clause: The truth condition for the strict implication $p \to q$ is defined such that $w \Vdash p \to q$ if and only if for all $w' \succeq w$ , if $R[w'] \subseteq \llbracket p \rrbracket$ , then $R[w'] \subseteq \llbracket q \rrbracket$ . This clause enforces upward persistence directly.
Upward-Flat Frames: To simplify correspondence results, the authors introduce "upward-flat" frames where $R$ is closed under post-composition with $\preceq$ (i.e., $w R v \preceq u \implies w R u$ ). They prove that any flat frame can be transformed into an upward-flat frame without changing its complex algebra, preserving the logic's validity.
Canonical Model Construction: To prove completeness and the FMP, the authors adapt the canonical model construction used for the logic $CK$ (conditional logic). Instead of using prime theories as worlds, they utilize segments. A segment is a pair $(\Gamma, U)$ where $\Gamma$ is a prime theory and $U$ is a set of prime theories encoding the successors. This "segment" approach allows for a finer-grained handling of the modal accessibility relation.
Handling Extensions: For extensions involving the axiom $4a$ (corresponding to transitivity), the authors modify the canonical model by restricting the set of segments to "pointed" segments (those generated by a specific formula $\gamma$ ) to ensure the transitivity of the accessibility relation in the canonical model.

Key Contributions and Results

Relational Semantics: The paper provides the first Kripke-style relational semantics for $HLC^\flat$ . It demonstrates that this semantics is sound and that the logic is complete with respect to the class of flat frames.
Completeness and FMP: Using the segment-based canonical model, the authors prove strong completeness and the finite model property for $HLC^\flat$ and several of its axiomatic extensions.
Correspondence Theory: The paper establishes frame correspondents for several axioms on upward-flat frames:
- $em $($ p \lor \neg p$) corresponds to $\preceq$ being symmetric.
- $t\Box$ ( $( \top \to p) \to p$ ) corresponds to the reflexivity of $\preceq \circ R$ .
- $str $($ (p \to q) \to (p \to q)$) corresponds to $R \subseteq \preceq$ .
- $4a$ ( $p \to (\top \to p)$ ) corresponds to the transitivity of $R$ .
- $pa $($ (p \to q) \to (\top \to (p \to q))$) corresponds to a specific condition involving the existence of intermediate worlds.
Embedding Sharp Logic: The authors show that the sharp logic $HLC^\sharp$ can be embedded into the flat semantics via a truth-preserving transformation of sharp frames into pointwise downward-directed flat frames, thereby recovering completeness for $HLC^\sharp$ within the new framework.
Extension Stability: The paper investigates the notion of extension stability (related to open subframes). It demonstrates that while the flat base calculus $HLC^\flat$ is extension stable, the sharp calculus $HLC^\sharp$ is not. This is shown semantically by constructing a flat model that validates $di$ (the sharpness axiom) but whose open subframe (induced by removing a specific world) fails to validate $di$.

Significance
The paper claims to fill a significant gap in the literature by providing a simple, Kripkean interpretation for flat Heyting-Lewis logic, which was previously elusive. This new semantics facilitates the derivation of completeness and finite model property results for $HLC^\flat$ and its extensions, which were previously only available via algebraic methods or more complex semantic frameworks.

The authors highlight that their semantics is particularly valuable for applications where the "sharp" axiom $di$ is not valid, such as in the study of arrows in functional programming (specifically those without choice) and in the schematic logics of arithmetical theories like Peano Arithmetic. By distinguishing between flat and sharp systems, the semantics clarifies why certain classical or sharp properties fail in these contexts. Furthermore, the work opens the door to studying duality and subframe constructions in the context of intuitionistic modal logics with strict implication, suggesting that the segment-based approach may be essential for a proper duality theory in this setting.