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.1 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 .
Proposition
A modal algebra refutes a stable canonical rule iff there is a stable embedding that satisfies the BDC for .
This result illustrates the connection between stable canonical rules and filtrations: a filtration of a model through a set of formulas always stably embeds into the original model through a map that satisfies the BDC for .
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.
Axiomatization
Let be a modal algebra and let be a modal rule. There are only finitely many pairs satisfying the following condition:
- is a modal algebra generated, as a Boolean algebra, by a set of cardinality equal to , where consists of the subformulas of formulas that are either premises or conclusions of ;
- for some valuation such that the model refutes in .
Let be the set of such pairs. If refutes , then there is a finite filtration of that also refutes . Moreover, the pair with defined from as above, belongs to , and the inclusion embedding is stable and satisfies the BDC for . So, refutes .
Conversely, take and assume refutes . Then there is a stable embedding satisfying the BDC for . Letting , where is the valuation on that “determines” as per the second item above, we obtain a model that refutes .
We have thus established:
Theorem
Every modal rule is equivalent to finitely many stable canonical rules.
Corollary
Every normal modal rule system is axiomatizable by stable canonical rules.
Footnotes
-
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. ↩