Stable Canonical Rules and Formulas for Pre-transitive Logics via Definable Filtration

This paper generalizes the theory of stable canonical rules and formulas to pre-transitive logics by introducing definable filtration, thereby establishing axiomatization, the finite model property, and structural characterizations for extensions of $\mathsf{K4^{m+1}_{1}}$ while demonstrating the existence of continuum many such logics that are neither $\mathsf{K4}$-stable nor subframe logics.

The Gist

Imagine you are trying to understand a massive, chaotic library of books (which represents the world of modal logic). Each book contains rules about how things can be connected, possible, or necessary. Some books are very strict and orderly (like transitive logics, where if A connects to B, and B to C, then A definitely connects to C). Others are messier and more flexible (pre-transitive logics), where connections might skip a step or behave differently.

For a long time, mathematicians had a powerful tool to organize the strict, orderly books called Canonical Formulas. Think of these as "ID cards" for specific patterns in the library. If you have the right ID card, you can instantly tell if a book belongs to a certain section. However, these ID cards broke down when applied to the messier, pre-transitive books. The standard method of creating these cards (called "filtration") was like trying to compress a high-definition movie into a tiny file; for the messy books, the compression ruined the picture, and the rules no longer made sense.

Tenyo Takahashi's paper introduces a new, smarter way to compress these files without losing the picture. Here is the breakdown of the paper's journey:

1. The Problem: The "Filtration" Filter

Imagine you have a giant map of a city (a Kripke model) with millions of intersections. To study it, you want to shrink it down to a small, manageable model.

• Standard Filtration: This is like taking a photo of the city and blurring it until only the major landmarks remain. You group nearby streets together. For orderly cities (transitive logics), this works perfectly. But for the messy, pre-transitive cities, the blurring creates "ghost streets" that don't actually exist, breaking the logic.
• The Issue: The standard method forces you to use the same list of landmarks to decide how to group the streets and how to draw the new roads. In messy logics, this creates a contradiction.

2. The Solution: "Definable Filtration"

Takahashi introduces a technique called Definable Filtration.

• The Analogy: Imagine you are organizing a messy closet.
  • Standard Filtration: You group clothes by color (the "equivalence relation") and then decide how to hang them based on that same color list.
  • Definable Filtration: You use a super-detailed list (a larger set of formulas) to group the clothes together (so you don't mix up a red shirt with a red sock). But, when you decide how to hang them on the rack (the "accessibility relation"), you only look at a simpler, core list of rules.
• Why it works: By using a finer, more detailed list to group things, you avoid the "ghost streets" problem. You get a small, finite map that still perfectly preserves the logic of the original messy city. This proves that even these messy logics have the Finite Model Property (meaning you can always find a small, finite example to test them).

3. The New ID Cards: Stable Canonical Rules & Formulas

Once the map is shrunk correctly, Takahashi creates new "ID cards" called Stable Canonical Rules and Formulas.

• The Metaphor: Think of these as blueprints. Instead of just saying "This building is a house," the blueprint says, "If you see a structure that looks exactly like this specific arrangement of rooms (a finite algebra), then it must follow these rules."
• The Breakthrough: Previously, these blueprints only worked for the strict, orderly logics (like K4). Takahashi shows that by using the new "Definable Filtration" method, these blueprints can now describe the messy, pre-transitive logics (specifically K4m+1 1).
• The Result: Every extension of these messy logics can be built using these blueprints. It's like saying, "No matter how complex your messy city is, we can describe it entirely using a finite set of Lego instructions."

4. The "Super-Blueprints": m-Stable Canonical Formulas

The paper goes one step further. It realizes that for these specific messy logics, the standard blueprints are a bit "overkill" or slightly off-target.

• The Analogy: Imagine the standard blueprint checks if a door is open or closed (1 step). But in these messy logics, the door might take 2 or 3 steps to fully open.
• The Innovation: Takahashi introduces m-Stable Canonical Formulas. These are "super-blueprints" that check the state of the system not just for 1 step, but for m steps (where m is a specific number related to the logic).
• Why it's better: These super-blueprints are more efficient. They are a smaller, tighter subset of the original blueprints that fit the "nature" of the messy logic perfectly. They are like a custom-tailored suit instead of an off-the-rack one.

5. The Big Picture: What Does This Mean?

• New Classes of Logic: The paper proves there are "continuum many" (an infinite, uncountable number) of these new logics. They are distinct from the old, well-known types. It's like discovering a whole new continent of mathematical islands.
• Solving Old Mysteries: It helps solve long-standing open problems about whether these logics can be decided by a computer (decidability) and how they fit into the "lattice" (the family tree) of all possible logics.
• Splitting the Family: The paper identifies specific "splitting" logics—these are the "boundary lines" in the family tree that separate different branches of logic.

Summary

In simple terms, Takahashi took a tool that was broken for messy, non-linear logical systems and fixed it by inventing a smarter way to compress data (Definable Filtration). This allowed him to create a new set of universal "blueprints" (Stable Canonical Formulas) that can describe these messy systems perfectly. He even upgraded these blueprints to be more precise (m-Stable), opening the door to understanding a vast, previously uncharted territory of logical systems.

The takeaway: We now have a better map and better instructions for navigating the complex, messy corners of the logical universe, proving that even the most chaotic systems can be understood through finite, structured rules.

Technical Summary

Here is a detailed technical summary of the paper "Stable Canonical Rules and Formulas for Pre-transitive Logics via Definable Filtration" by Tenyo Takahashi.

1. Problem Statement

The paper addresses a significant gap in the theory of modal logics, specifically concerning pre-transitive logics.

• Context: Characteristic formulas (like Jankov formulas, canonical formulas, and stable canonical formulas) are powerful tools for analyzing the lattice of modal logics. They allow logics to be axiomatized and properties like the Finite Model Property (FMP) to be proven.
• The Gap: While the theory of stable canonical rules and formulas is well-established for transitive logics (specifically $K4$ and extensions), it fails to generalize to pre-transitive logics (logics satisfying $m$-transitivity conditions like $\Diamond^{m+1}p \to \Diamond^m p \lor \dots \lor p$).
• The Obstacle: The standard method for constructing characteristic formulas relies on filtration (specifically selective or standard filtration). However, standard filtration techniques do not easily apply to pre-transitive logics (e.g., $K4^m_1$). The equivalence relations used in standard filtration often fail to preserve the necessary stability conditions (order-preservation) required for the quotient map to be a stable morphism in non-transitive settings.
• Open Problems:
  • The decidability of the admissibility problem for pre-transitive logics is open.
  • The FMP for general pre-transitive logics is a long-standing open problem.
  • No known variant of subframe formulas or stable canonical formulas exists for these logics.

2. Methodology

The author introduces and utilizes definable filtration as the core methodological innovation to overcome the limitations of standard filtration.

• Definable Filtration: This is a generalization of standard filtration.
  • Standard Filtration: Uses a set of formulas $\Theta$ to define both the equivalence relation (identifying points agreeing on $\Theta$) and the accessibility relation in the quotient.
  • Definable Filtration: Uses a larger set $\Theta' \supseteq \Theta$ to define the equivalence relation (creating a finer partition) but retains $\Theta$ to determine the constraints on the accessibility relation.
  • Key Advantage: This "mismatch" allows the construction of finite quotients that preserve the specific algebraic properties of pre-transitive logics, which standard filtration cannot do.
• Algebraic Framework: The paper works primarily within the duality between modal algebras and modal spaces (descriptive frames).
  • It generalizes stable homomorphisms and the Closed Domain Condition (CDC).
  • It introduces the $m$-Closed Domain Condition ($m$-CDC), which requires homomorphisms to preserve modalities up to $m$ steps, matching the nature of pre-transitive logics.
• Gabbay's Filtration: The author provides an algebraic proof that Gabbay's filtration (originally defined for frames) works for the logic $K4^m_1 = K + \Diamond^{m+1}p \to p$ (for $m \ge 1$), showing these logics admit definable filtration.

3. Key Contributions

A. Generalization of Stable Canonical Rules

The paper proves that for any modal logic or rule system that admits definable filtration, every extension is axiomatizable by stable canonical rules.

• This generalizes previous results (which were limited to $SK$ and $K4$) to a broader class of logics.
• It establishes that if a logic admits definable filtration, it possesses the Finite Model Property (FMP).

B. Development of Stable Canonical Formulas for $K4^m_1$

The author constructs stable canonical formulas specifically for the pre-transitive logics $K4^m_1$.

• Master Modality: The construction relies on the fact that the "master modality" (a modality capturing the transitive closure or pre-transitive closure) is definable in $K4^m_1$.
• Axiomatization: It is shown that every extension of $K4^m_1$ can be axiomatized by stable canonical formulas.
• $m$-Stable Canonical Formulas: A stricter subclass of formulas is introduced. These formulas encode the structure of finite modal algebras up to $m$ steps using the $m$-CDC. The paper proves that these $m$-stable formulas are sufficient to axiomatize all extensions of $K4^m_1$, offering a more "natural" fit for pre-transitive logics than the general stable formulas.

C. Structural Characterizations

The paper provides deep structural insights into the lattice of extensions of $K4^m_1$ ($NExtK4^m_1$):

1. FMP for Stable Logics: It proves that all $K4^m_1$-stable logics (logics axiomatized by stable formulas) have the FMP.
2. Continuum Many New Logics: The author constructs continuum many $K4^m_1$-stable logics that are:
   • Not $K4$-stable.
   • Not subframe logics.
   • Distinct for different $m$ (i.e., they do not contain $K4^{m'}_1$ for $m' < m$).
3. Splitting Logics: It characterizes splitting and union-splitting logics in the lattice $NExtK4^m_1$ using Jankov formulas (a specific type of stable canonical formula where the domain set is the whole algebra).

4. Key Results

• Theorem 3.9 & 3.10: Generalized axiomatization theorem. Any rule system or logic admitting definable filtration is axiomatizable by stable canonical rules/formulas over its base.
• Theorem 4.3: The logic $K4^m_1$ admits definable filtration (proven algebraically).
• Corollary 4.4: $K4^m_1$ has the FMP.
• Theorem 5.7: Every logic $L \supseteq K4^m_1$ is axiomatizable by stable canonical formulas.
• Theorem 5.12 & 5.17:
  • Every $K4^m_1$-stable logic has the FMP.
  • There are continuum many $K4^m_1$-stable logics that are neither $K4$-stable nor subframe logics.
• Theorem 6.11: Every extension of $K4^m_1$ is axiomatizable by $m$-stable canonical formulas (a proper subclass of stable canonical formulas).

5. Significance

• Bridging the Gap: This work successfully extends the powerful machinery of stable canonical formulas from transitive logics to the more complex pre-transitive setting, a domain where such tools were previously unavailable.
• Solving Open Problems: It resolves the FMP for the specific class of $K4^m_1$-stable logics and provides a new large class of non-transitive logics with the FMP.
• Methodological Advancement: By formalizing definable filtration and $m$-CDC, the paper provides a robust algebraic framework that can potentially be applied to other non-transitive logics where standard filtration fails.
• Future Directions: The results lay the groundwork for tackling the decidability of the admissibility problem in pre-transitive logics, a major open problem in modal logic. The paper suggests that stable canonical rules could be the key to proving decidability for $K4^m_1$, similar to how they were used for $K4$ and $S4$.

In summary, Takahashi's paper is a foundational step in generalizing the theory of characteristic formulas to non-transitive logics, utilizing definable filtration to construct a rich theory of stable canonical rules and formulas for pre-transitive systems.