Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Hereditarily Structurally Complete Superintuitionistic Logics and Primitive Varieties of Heyting Algebras

Alex Citkin

TL;DR

The paper provides an algebraic proof that hereditary structural completeness of intermediate logics corresponds to primitiveness of the associated Heyting-algebra varieties, with prohibited algebras P1–P5 serving as the dividing criterion. It identifies W, the largest variety omitting all prohibited algebras, as the maximal primitive (hereditarily structurally complete) variety, and proves that W is locally finite with all subvarieties finitely based. Through well quasi-ordering techniques and projectivity analyses, the authors establish an explicit algorithm to decide primitivity from finite sets of equations and show that every primitive variety is contained in W (and thus finitely based). The work also clarifies the relationship between primitive and structurally complete logics, situates Md as a broader ambient class, and outlines open problems about the existence and nature of structurally complete but non-primitive varieties outside Md. Overall, the results provide a complete, countable framework for primitive varieties of Heyting algebras and their finite bases, with practical consequences for axiomatization and decidability of primitivity.

Abstract

We give an algebraic proof of the criterion for hereditary structural completeness of an intermediate logic, or, equivalently, of the primitiveness of a variety of Heyting algebras.

Hereditarily Structurally Complete Superintuitionistic Logics and Primitive Varieties of Heyting Algebras

TL;DR

The paper provides an algebraic proof that hereditary structural completeness of intermediate logics corresponds to primitiveness of the associated Heyting-algebra varieties, with prohibited algebras P1–P5 serving as the dividing criterion. It identifies W, the largest variety omitting all prohibited algebras, as the maximal primitive (hereditarily structurally complete) variety, and proves that W is locally finite with all subvarieties finitely based. Through well quasi-ordering techniques and projectivity analyses, the authors establish an explicit algorithm to decide primitivity from finite sets of equations and show that every primitive variety is contained in W (and thus finitely based). The work also clarifies the relationship between primitive and structurally complete logics, situates Md as a broader ambient class, and outlines open problems about the existence and nature of structurally complete but non-primitive varieties outside Md. Overall, the results provide a complete, countable framework for primitive varieties of Heyting algebras and their finite bases, with practical consequences for axiomatization and decidability of primitivity.

Abstract

We give an algebraic proof of the criterion for hereditary structural completeness of an intermediate logic, or, equivalently, of the primitiveness of a variety of Heyting algebras.

Paper Structure

This paper contains 26 sections, 67 theorems, 58 equations, 13 figures, 2 tables.

Table of Contents

  1. Introduction.
  2. Preliminaries.
  3. Heyting Algebras: Definitions and Properties.
  4. Coatoms.
  5. Ordinary elements.
  6. Strong partial ordering.
  7. Nodes.
  8. Coalesced Ordinal Sums.
  9. Subdirect products.
  10. Finitely Generated Heyting Algebras: Definitions and Properties.
  11. One-generated Heyting Algebras.
  12. Finitely Generated Heyting Algebras.
  13. Criterion of local finiteness
  14. Primitive Varieties: Definitions and Properties.
  15. Weakly projective algebras.
  16. ...and 11 more sections

Key Result

Theorem 1.1

An si-logic $\mathsf{L}$ is hereditarily structurally complete if and only if none of the prohibited algebras ${\textbf{\upshape P}}_i$, $i \in [1,5]$ (whose Hasse diagrams are depicted in Fig. fig-alg) is a model of $\mathsf{L}$.

Figures (13)

  • Figure 1: Prohibited Algebras.
  • Figure 2: Subalgebra generated by the coatoms.
  • Figure 3: Subalgebra
  • Figure 4: Counterexamples.
  • Figure 5: One-generated Heyting algebras.
  • ...and 8 more figures

Theorems & Definitions (106)

  • Theorem 1.1: Citkin_1978
  • Theorem 1.2
  • Theorem 1.3
  • Theorem 1.4
  • Theorem 1.5
  • Theorem 1.6
  • Theorem 1.7
  • Proposition 2.1
  • Proposition 2.2
  • proof
  • ...and 96 more