Stable canonical rule

Idea

A stable canonical rule is a rule that syntactically encodes the structure of a finite algebra in a particular way. They are useful because they have well behaved refutation conditions: a stable canonical rule representing the structure of an algebra is refuted by precisely those algebras such that there is a stable embedding from to satisfying a certain condition.

Stable canonical rules were introduced in @BezhanishviliBezhanishvili2017LFRoHAaCF and @BezhanishviliEtAl2016SCR. They are related to the canonical formulas and rules of @Zakharyaschev1992CFfKPIBR and @Jerabek2009CR.

Definition

To illustrate, let’s take the case of stable canonical rules for modal algebras.¹ Given a modal algebra , a domain on is just a finite subset . Work in a language equipped with a propositional variable for each . The stable canonical rule is defined as the rule , where

Thus the rule fully represents the Boolean structure of , but only partially represents the modal structure of . The behavior of is only fully represented for elements belonging to the domain .

Refutation conditions and duality

Given modal algebras , a stable embedding is an embedding which partially preserves , in the sense that holds for all . Given a domain , we say that satisfies the bounded domain condition (BDC) for when fully preserves on : the identity holds for all .

Via duality, we can characterize the refutation conditions of stable canonical rules on modal spaces (descriptive Kripke frames) as well. When are modal spaces, a map is called stable when it is continuous and relation preserving. A domain on is any finite set of clopens in . Given a domain on , we say that satisfies the bounded domain condition (BDC) for when the following holds: for each and any , if there is some such that , then there must be some such that and .

Note that when is finite and we take to contain precisely the singletons of points in , a stable map satisfying the BDC for is nothing but a bounded morphism from to .

When is a modal algebra, let be its dual modal space. Let be the Stone map, which sends an element of to the set of prime filters containing it.

Proposition

A modal space refutes a stable canonical rule iff there is a stable surjection satisfying the BDC for .

This justifies writing a stable canonical rule as , with constructed from as above.

Footnotes

1. Stable canonical rules can also be developed for Heyting and bi-Heyting algebras, frontal Heyting algebras, Boolean algebras with operators, and probably many more kinds of algebras. ↩