Pre-filtrations, Pre-stable Canonical Rules, and the Kuznetsov-Muravitsky Isomorphism

Basic Information

• Paper ID: 2511.09824
• Title: Pre-filtrations, Pre-stable Canonical Rules, and the Kuznetsov-Muravitsky Isomorphism
• Authors: Nick Bezhanishvili, Antonio Maria Cleani
• Classification: math.LO (Mathematical Logic)
• Publication Date: November 14, 2025
• Paper Link: https://arxiv.org/abs/2511.09824

Abstract

This paper introduces the concepts of pre-filtrations and pre-stable canonical rules for the Kuznetsov-Muravitsky system of intuitionistic modal logic, and provides a new proof of the Kuznetsov-Muravitsky isomorphism theorem along with several preservation results. The proofs employ these rules and the duality between modal (Heyting) algebras and their corresponding ordered topological spaces.

Research Background and Motivation

Research Questions

This paper investigates the structural properties of the Kuznetsov-Muravitsky logical system (KM), particularly its isomorphic relationship with the modal provability logic GL. The core questions include:

1. How to understand the KM system as the "true intuitionistic counterpart" of GL
2. How to establish a complete lattice isomorphism between the lattice of normal extensions of KM and that of GL
3. How to prove relevant preservation results (such as preservation of Kripke completeness and finite model property)

Significance of the Problem

According to Kuznetsov's perspective, understanding a logical system requires understanding the behavior of that system and its "neighbors" (i.e., extensions of the logic). From this viewpoint, the true intuitionistic counterpart of GL should be a system whose lattice of normal extensions is isomorphic to that of GL. The KM system is precisely such a system. This isomorphic relationship was first proved by Kuznetsov and Muravitsky in the 1980s, known as the Kuznetsov-Muravitsky isomorphism.

Limitations of Existing Approaches

Standard filtration methods encounter fundamental difficulties in both KM and GL systems:

1. Problem with GL: Certain GL spaces (such as the example X in the paper, containing a non-trivial cluster of two reflexive points) must contain reflexive points in the image under any stable mapping, but finite GL spaces cannot contain reflexive points
2. Problem with KM: Similarly, certain KM spaces must contain reflexive points under the modal relation in the image under relation-preserving mappings, but finite KM spaces cannot contain such points
3. This causes standard filtration to fail in proving the finite model property for these systems

Research Motivation

The motivation for this paper is to:

1. Overcome the limitations of standard filtration and develop new techniques applicable to KM and GL systems
2. Provide a new proof method for the Kuznetsov-Muravitsky isomorphism
3. Establish a theoretical framework based on algebraic rules for studying extensions of the KM system
4. Prove relevant preservation theorems and refine understanding of the KM system

Core Contributions

The main contributions of this paper include:

1. Introduction of the pre-filtration concept: This is a generalization of standard filtration that, by weakening certain preservation requirements, becomes applicable to KM and GL systems
2. Development of pre-stable canonical rules theory:
   • Establishes an algebraic rule system for KM and GL systems
   • Proves that every rule is equivalent to finitely many pre-stable canonical rules
3. Provision of a new proof of the Kuznetsov-Muravitsky isomorphism:
   • Uses pre-stable canonical rules and duality theory
   • Proves complete lattice isomorphism between NExt(KM) and NExt(GL)
4. Proof of Esakia's theorem: Establishes complete lattice isomorphism between NExt(mHC) and NExt(K4.Grz)
5. Establishment of preservation results: Proves that the mapping σ from KM to GL preserves Kripke completeness and finite model property
6. Skeleton generation theorem: Proves that every universal class of K4.Grz algebras is generated by its skeleton elements

Methodology Details

Task Definition

The core task of this paper is to establish structural correspondence between the intuitionistic modal logic system KM and the classical modal logic system GL. Specifically:

• Input: Rule systems, algebraic classes, or space classes
• Output: Isomorphic mappings, preservation theorems, equivalence results
• Constraints: Must work within the lattice structure of normal extensions while preserving algebraic and topological properties of logical operations

Core Conceptual Architecture

1. Pre-stable Embedding

Definition: For frontal Heyting algebras or K4 algebras A, B, an injection h: A → B is called a pre-stable embedding if:

• Frontal Heyting case: h is a bounded distributive lattice embedding
• K4 case: h is a Boolean embedding satisfying h(□⁺a) ≤ □⁺h(a)

Key Innovation: Compared to stable embeddings, pre-stable embeddings do not require partial preservation of ⊠ and □ operators, only preservation of the □⁺ operator. This weakening is the crucial technical breakthrough.

2. Bounded Domain Condition (BDC)

For a unary or binary operator ⊙ and domain D, a mapping h satisfies BDC⊙ if and only if it completely preserves ⊙ on elements in D:

• Unary case: h(⊙a) = ⊙h(a) for all a ∈ D
• Binary case: h(a⊙b) = h(a)⊙h(b) for all (a,b) ∈ D

3. Back and Forth Condition (BFC)

For a relation ≺ and domain D, a pre-stable mapping f: X → Y satisfies BFC≺ when:

• Back: If there exists y ∈ d such that f(x) ≺ y, then there exists z ∈ X such that x ≺ z and f(z) ∈ d
• Forth: If there exists y ∈ f⁻¹(d) such that x ≺ y, then there exists z ∈ d such that f(x) ≺ z

Pre-filtration Construction Method

Sim Case (Frontal Heyting Algebras)

Given a fronton H, valuation V, and subformula-closed set Θ, construct a pre-filtration (K, V'):

Steps:

1. Let K₀ be the bounded distributive sublattice generated by VΘ
2. Enumerate D⊠ := {V(φ) : ⊠φ ∈ Θ} = {a₁, ..., aₖ}
3. Define recursively:
   • Cᵢ₊₁ := {(b → aᵢ₊₁) ∧ ⊠aᵢ₊₁ : b ∈ Kᵢ ∩ aᵢ₊₁, ⊠aᵢ₊₁}
   • Kᵢ₊₁ is the bounded sublattice generated by Kᵢ ∪ Cᵢ
4. Let K := Kₖ, using the Heyting algebra unique extension theorem to define → and ⊠

Key Properties:

• The inclusion embedding ⊆: K → H is a pre-stable embedding
• Satisfies BDC→ and BDC⊠
• K is a fronton

Clm Case (K4 Algebras)

For K4 algebra M and Θ, the pre-filtration construction directly uses the Boolean subalgebra generated by VΘ, with appropriate □ operator definition. The key point is that only □⁺ needs to be preserved, not □.

Pre-stable Canonical Rules

Sim Pre-stable Canonical Rule η(H, D)

For finite frontal Heyting algebra H and domain D = (D→, D⊠):

Premises Γ include:

• {p₀ ↔ ⊥, p₁ ↔ ⊤} (boundary conditions)
• {pₐ∧ᵦ ↔ pₐ ∧ pᵦ, pₐ∨ᵦ ↔ pₐ ∨ pᵦ} (lattice structure)
• {pₐ→ᵦ ↔ pₐ → pᵦ : (a,b) ∈ D→} (implication on domain)
• {p⊠ₐ ↔ ⊠pₐ : a ∈ D⊠} (modality on domain)

Conclusions Δ:

• {pₐ ↔ pᵦ : a ≠ b} (separation of distinct elements)

Clm Pre-stable Canonical Rule µ(M, D)

Defined similarly, but using Boolean structure and □⁺, □ operators.

Technical Innovations

1. Weakening of preservation requirements: Pre-stable embeddings only require preservation of □⁺ rather than □, allowing handling of spaces containing reflexive points
2. Classicizable rules: Introduction of special sim canonical rules where D→ can be embedded into D⊠, creating natural correspondence between the two domains
3. Cluster collapse technique: In proving the main lemma, construct pre-stable mappings by collapsing clusters while preserving the BFC condition
4. Skeleton generation: Proves that every universal class of K4.Grz algebras is generated by its skeleton elements (Theorem 5.9), which is key to proving the isomorphism
5. Rule characterization of translation mapping T: Characterize the action of translation mapping T through classicization µ◦(F,D) of classicizable rules

Experimental Setup

This paper is pure mathematical theory research and does not involve experimental setup, datasets, or numerical experiments. All results are obtained through rigorous mathematical proofs.

Main Theorems and Proof Strategies

Theorem 3.16 (Existence of Pre-filtration)

Statement: For any fronton H, model (H, V), and subformula-closed set Θ, there exists a pre-filtration (K, V') based on a fronton K.

Proof Strategy:

1. Use the unique extension construction of Theorem 3.13
2. Ensure BDC conditions by iteratively adding Boolean complements
3. Utilize the special property of frontons (⊠a → a ≤ a)

Theorem 4.5 (Rule Equivalence)

Statement: Every sim rule (resp. clm rule) on KM (resp. K4) is equivalent to finitely many pre-stable canonical rules.

Proof Outline:

1. For the algebra of a counterexample rule Γ/∆, construct its pre-filtration
2. Generate pre-stable canonical rules from the pre-filtration
3. Prove that the original rule is counterexampled if and only if some pre-stable canonical rule is counterexampled
4. Ensure only finitely many rules are needed through local finiteness

Theorem 5.8 (Main Lemma)

Statement: For K4.Grz space X and clm rule Γ/∆, X ̸|= Γ/∆ if and only if σρX ̸|= Γ/∆.

Proof Core:

1. Assume existence of pre-stable surjection f: X → F counterexampling the rule
2. For each cluster C ⊆ F, construct disjoint clopen sets Uᵢ covering ϱf⁻¹(C)
3. Define mapping g: σρX → F, using separating sets on clusters
4. Verify that g preserves R⁺ and satisfies BFC condition
5. Crucially use properties of max(f⁻¹(d)) and Lemma 3.11

Theorem 5.9 (Skeleton Generation Theorem)

Statement: Every universal class U of K4.Grz algebras is generated by its skeleton elements, i.e., U = σρU.

Proof: Directly follows from Main Lemma 5.8 and Completeness Theorem 2.2.

Theorem 5.13 (Esakia's Theorem)

Statement: The mappings σ and ρ|_{NExt(K4.Grz)} are mutually inverse complete lattice isomorphisms between NExt(mHC) and NExt(K4.Grz).

Proof Structure:

1. Prove that semantic mappings σ: Uni(fHA) → Uni(K4.Grz) and ρ are order-preserving
2. Use skeleton generation theorem to prove ρσU = U
3. Use Proposition 5.3 to prove σρV = V
4. Verify preservation of infinite joins

Corollary 5.14 (Kuznetsov-Muravitsky Isomorphism)

Statement: σ|{NExt(KM)} and ρ|{NExt(GL)} are mutually inverse complete lattice isomorphisms between NExt(KM) and NExt(GL).

Proof: Directly follows from Esakia's Theorem and the observation that σKM = GL.

Theorem 6.7 (Pre-filtration for Magari Algebras)

Statement: For Magari algebra M, if M ̸|= Γ/∆, then there exists a pre-filtration based on a Magari algebra N.

Proof Strategy:

1. First construct a counterexample model on σρM
2. Decompose elements as Boolean combinations of quasi-open elements
3. Construct fronton K on ρM
4. Return to Magari algebra via σK
5. Use Lemma 6.6 to ensure BDC conditions

Theorem 6.10 (Preservation Theorems)

Statement: For L ∈ NExt(KM):

1. L is Kripke complete if and only if τL is Kripke complete
2. L has finite model property if and only if τL has finite model property

Proof Outline:

1. Use Kripke frames and pre-stable canonical rules
2. Convert back and forth between sim and clm frames
3. Utilize special properties of classicizable rules
4. Apply Theorem 6.8 on equivalence of classicized rules

Related Work

Historical Background

1. Original Kuznetsov-Muravitsky work 19, 20, 22, 28, 29: First established the isomorphism between KM and GL using proof-theoretic methods
2. Esakia's contributions 14:
   • First proposed modalized Heyting calculus (mHC)
   • Announced the isomorphism between mHC and K4.Grz (Esakia's Theorem)
   • Provided an algebraic perspective on the KM system
3. Blok-Esakia isomorphism 6: Complete lattice isomorphism between superintuitionistic logics and normal extensions of Grz, providing a template for this paper's work

Related Proof Methods

1. Litak's work 25: Provided a proof of Esakia's Theorem, discussed monomodal companions
2. Muravitsky's subsequent work 27, 31, 32:
   • Extended Kuznetsov's proof
   • Investigated connections between extension lattices of different logical systems
   • Provided variants of filtration constructions
3. Stable canonical rules 2, 3:
   • Techniques developed by Bezhanishvili et al.
   • Predecessors of this paper's pre-stable rules
   • Successfully applied to new proof of Blok-Esakia isomorphism 4

Positioning of This Paper

Advantages of this paper compared to existing work:

1. Unified framework: Provides unified treatment using pre-stable canonical rules
2. New proof techniques: Overcomes limitations of standard filtration
3. Stronger results: Proves not only isomorphism but also preservation theorems
4. Algebraic perspective: Entirely based on algebra and duality theory, avoiding complex syntactic operations

Conclusions and Discussion

Main Conclusions

1. Effectiveness of pre-filtration: Pre-filtration successfully overcomes fundamental obstacles of standard filtration in KM and GL systems, providing effective finite model construction methods for these systems
2. New proof of Kuznetsov-Muravitsky isomorphism: Through pre-stable canonical rules and duality theory, provides a new proof path for this classical result, demonstrating the power of algebraic methods
3. Establishment of Esakia's Theorem: Completely proves the lattice isomorphism between NExt(mHC) and NExt(K4.Grz), filling an important theoretical gap
4. Preservation results: Proves that mapping σ preserves Kripke completeness and finite model property, deepening understanding of KM system structure
5. Establishment of theoretical framework: Establishes a complete algebraic rule-based theoretical framework for KM systems and their extensions

Limitations

1. Restricted scope of applicability:
   • Pre-stable canonical rule theory is primarily aimed at KM and its extensions
   • For general extensions of mHC, existence of pre-filtration remains an open problem
   • Unclear how to generalize to signatures containing multiple non-interdefinable operators
2. Constructivity issues:
   • The size bound of finite set Ψ in Theorem 6.8 is non-constructive
   • Relies on compactness arguments without providing explicit bounds
3. Technical complexity:
   • Introduction of classicizable rules increases technical complexity
   • Requires conversion back and forth between sim and clm rules
   • Proofs employ multi-level algebraic and topological structures
4. Open problems:
   • Existence of pre-filtration for all extensions of mHC (generalization of Theorem 3.16)
   • Filtration theory in multi-operator signatures
   • Development of pre-stable logic theory (analogous to stable logic theory 2,3)

Future Directions

The paper explicitly proposes the following research directions:

1. Pre-stable logic theory: Develop KM pre-stable logic theory analogous to stable logic, investigating which KM extensions are pre-stable
2. Concrete axiomatization: Obtain explicit axiomatizations of concrete KM extensions using pre-stable canonical rules
3. Other intuitionistic modal logics: Explore applications of pre-stable canonical rules in other KM-like logics, particularly those where standard filtration fails
4. Complete theory of mHC: Extend algebraic rule theory to all extensions of mHC, not just KM extensions
5. Multi-operator systems: Investigate filtration construction in signatures containing multiple non-interdefinable operators

In-Depth Evaluation

Strengths

1. Methodological Innovation

• Conceptual breakthrough: Introduction of pre-stable embeddings and pre-filtrations is a genuine innovation, cleverly overcoming essential difficulties by precisely weakening standard concepts
• Technical sophistication: Techniques such as classicizable rules and cluster collapse demonstrate profound mathematical insight
• Unified framework: Organically combines algebraic, topological, and logical methods, providing a unified treatment perspective

2. Theoretical Depth

• Completeness: Proves not only isomorphism but also preservation theorems, forming a complete theoretical system
• Full utilization of duality theory: Freely converts between algebras and spaces, fully exploiting Stone duality and Esakia duality
• Skeleton generation theorem: A profound structural result with independent mathematical value

3. Proof Rigor

• Logical clarity: From basic definitions to main theorems, the argument chain is complete
• Complete technical details: Provides detailed proofs for key lemmas (such as 3.11, 6.2)
• Multi-level verification: Verifies key properties through both algebraic and dual perspectives

4. Academic Contribution

• Solves long-standing problems: Provides new technical tools for KM systems
• Generalizes classical results: Extends proof techniques of Blok-Esakia isomorphism to new domains
• Opens new directions: Provides clear directions for subsequent research

Weaknesses

1. Theoretical Limitations

• Narrow scope: Main results limited to KM and its extensions; treatment of general mHC extensions is incomplete
• Non-constructivity: Some existence results rely on compactness without constructive bounds
• Many open problems: Leaves several important open questions (such as complete generalization of Theorem 3.16)

2. Technical Complexity

• Multi-level structure: Involves rule systems, algebras, spaces, Kripke frames and other levels, creating a steep learning curve
• Heavy notation: Extensive mathematical notation and definitions may affect readability
• Lengthy proofs: Some proofs (such as Theorems 3.16, 5.8) involve complex constructions with numerous details

3. Practical Considerations

• Computability: Computational complexity of pre-stable canonical rules not discussed
• Algorithm implementation: No algorithmic guidance or implementation provided
• Application scenarios: Limited guidance for practical logical system design

Impact

Contributions to the Field

1. Methodological contribution: Provides new technical tools for studying intuitionistic modal logic
2. Theoretical refinement: Completes proof of Esakia's Theorem, filling important theoretical gap
3. Bridge function: Strengthens connections between intuitionistic logic and classical modal logic

Practical Value

• Finite model property: Provides methods for proving finite model property of KM extensions
• Decidability: Provides tools for investigating decidability problems
• Axiomatization: Provides approaches for finding axiomatizations of concrete extensions

Reproducibility

• Theoretical reproducibility: All proofs are pure mathematics, in principle completely verifiable
• Formalization potential: Clear structure suitable for formal verification (e.g., in Coq or Lean)
• Educational value: Can serve as advanced graduate course material

Applicable Scenarios

1. Theoretical research:
   • Studying extension lattice structures of intuitionistic modal logic
   • Exploring translations and embeddings between different logical systems
   • Developing new proof-theoretic and model-theoretic techniques
2. Metamathematical research:
   • Investigating metamathematical properties of logical systems (completeness, decidability, etc.)
   • Establishing correspondences between different logical systems
   • Studying relationships between algebraic and Kripke semantics
3. Potential applications:
   • Modal type theory in program verification
   • Intuitionistic modal logic in knowledge representation
   • Formalization of constructive mathematics

Key References

1. Esakia 14, 15: Foundational work on modalized Heyting calculus, core literature on duality theory
2. Kuznetsov & Muravitsky 19, 20, 22: Original papers on KM system, first proof of isomorphism theorem
3. Bezhanishvili et al. 2, 3, 4: Stable canonical rules theory, predecessors of this paper's methods
4. Litak 25: Alternative proof of Esakia's Theorem, theory of monomodal companions
5. Blok 6: Original work on Blok-Esakia isomorphism, providing template for this paper
6. Chagrov & Zakharyaschev 11: Standard textbook on modal logic, providing theoretical background

Overall Evaluation

This is a high-quality mathematical logic theory paper with substantial technical innovations and important theoretical contributions. The introduction of pre-stable canonical rules cleverly solves the problem of standard methods failing in KM and GL systems, demonstrating the authors' profound mathematical ability and innovative capacity. The paper not only provides new proofs of classical results but also establishes a complete theoretical framework, laying solid foundations for subsequent research.

Despite limitations in scope of applicability and technical complexity challenges, these shortcomings do not diminish the paper's core value. For scholars engaged in intuitionistic modal logic, algebraic logic, or modal logic research, this paper provides important technical tools and theoretical insights worthy of deep study and application.

Recommendation Index: ★★★★★ (5/5) Suitable Readers: Mathematical logic researchers, algebraic logic experts, modal logic theorists Reading Difficulty: High (requires solid background in algebra, topology, and logic)