View source for Sahlqvist identities

<!--
s1100201.png
$#A+1 = 22 n = 0
$#C+1 = 22 : ~/encyclopedia/old_files/data/S110/S.1100020 Sahlqvist identities
Automatically converted into TeX, above some diagnostics.
Please remove this comment and the {{TEX|auto}} line below,
if TeX found to be correct.
-->

{{TEX|auto}}
{{TEX|done}}

The counterpart in the theory of Boolean algebras with operators of Sahlqvist formulas (cf. [[Sahlqvist theorem|Sahlqvist theorem]]). Sahlqvist identities may be obtained from (modal) Sahlqvist formulas by viewing the latter as equations to be interpreted on Boolean algebras with operators (cf. [[Algebra of logic|Algebra of logic]]). For example, viewed algebraically, the (modal) Sahlqvist formula  $  \Diamond\Box p \rightarrow p $
becomes  $  \Diamond\Box x \leq  x $.

An explicit definition of Sahlqvist identities can be given as follows. Let  $  \Lambda = \{ {f _ {i} } : {i \in I } \} $
be a set of finitary (normal) additive operations. Let an untied term over  $  \Lambda $
be a term that is either:

i) negative (in the sense that every variable occurs in the scope of an odd number of complementation signs  $  - $
only);

ii) of the form  $  g _ {1} ( g _ {2} \dots ( g _ {n} ( x ) ) \dots ) $, 
where the  $  g _ {i} $'
s are duals of unary operators in  $  \Lambda $(
i.e.,  $  g _ {i} $
is defined by  $  g _ {i} ( x ) = - f _ {i} ( - x ) $
for some unary  $  f _ {i} $
in  $  \Lambda $);

iii) closed (i.e., without occurrences of variables); or

iv) obtained from terms of type i), ii) or iii) by applying  $  + $, 
$  \cdot $
and elements of  $  \Lambda $
only.

Then an identity is called a Sahlqvist identity if it is of the form  $  s = 1 $, 
where  $  s $
is obtained from complemented untied terms  $  - u $
by applying duals of elements of  $  \Lambda $
to terms that have no variables in common, and  $  \cdot $
only. For example, the above inequality  $  \dia \square x \leq  x $
can be rewritten as  $  - ( \dia \square x \cdot - x ) = 1 $, 
which is of the required form. As a further example, all standard axioms for both relation and cylindric algebras can be brought to Sahlqvist form.

The canonical extension of a Boolean algebra with operators is the complete and atomic extension obtained from the Stone representation of the algebra. The important feature of Sahlqvist identities is that they are preserved in passing from a Boolean algebra with operators to its canonical extension; the corresponding result for [[Modal logic|modal logic]] is known as the [[Sahlqvist theorem|Sahlqvist theorem]], cf. [[#References|[a5]]]. Identities with the latter property were first investigated in [[#References|[a3]]].

====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  R. Goldblatt,   "Varieties of complex algebras"  ''Ann. Pure and Applied Logic'' , '''44'''  (1989)  pp. 173–242</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  B. Jónsson,   "On the canonicity of Sahlqvist identities"  ''Studia Logica'' , '''53'''  (1994)  pp. 473–491</TD></TR><TR><TD valign="top">[a3]</TD> <TD valign="top">  B. Jónsson,   A. Tarski,   "Boolean algebras with operators I"  ''Amer. J. Math.'' , '''73'''  (1951)  pp. 891–939</TD></TR><TR><TD valign="top">[a4]</TD> <TD valign="top">  M. de Rijke,   Y. Venema,   "Sahlqvist's theorem for Boolean algebras with operators, with an application to cylindric algebras"  ''Studia Logica'' , '''54'''  (1995)  pp. 61–78</TD></TR><TR><TD valign="top">[a5]</TD> <TD valign="top">  H. Sahlqvist,   "Completeness and correspondence in the first and second order semantics for modal logic"  S. Kanger (ed.) , ''Proc. Third Scand. Logic Symp. Uppsala (1973)'' , North-Holland  (1975)  pp. 110–143</TD></TR></table>