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

  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.