Preservation of Sahlqvist fixed point equations in completions of relativized fixed point Boolean algebras with operators (Q1762482): Difference between revisions

The authors define Sahlqvist fixed-point equations and prove that every Sahlqvist fixed-point equation is preserved under completions of conjugated relativized fixed-point BAOs (Boolean algebras with operators). In the language of modal \(\mu\)-calculs, a set of fixed points of terms is defined recursively as follows: For a countable set \(V\) of variables and a set \(L\) of operators, {\parindent = 5mm \begin{itemize} \item[{\(\bullet\)}] constants \(\bot\) and \(\top\) and variables are fixed-point terms; \item [{\(\bullet\)}] if \(t_1\) and \(t_2\) are fixed-point terms, then so are \(t_1 \wedge t_2\), \(t_1 \vee t_2\), \(\neg t_1\); \item [{\(\bullet\)}] for each \(n\)-ary operator \(f\in L\) and fixed-point terms \(t_1, \ldots , t_n\), \(f(t_1, \ldots, t_n)\) is also a fixed-point term; \item [{\(\bullet\)}] for each fixed-point term \(\gamma(x, x_1, \ldots, x_n)\), where \(x\) occurs under the scope of an even number of negations, \(\mu x \gamma(x, x_1, \ldots, x_n)\) and \(\nu x \gamma(x, x_1, \ldots, x_n)\) are fixed-point terms. \end{itemize}} A fixed-point term which has no operators \(\mu\), \(\nu\) is called an \(L\)-term. A skeleton is a term \(\alpha (x_1, \ldots, x_n)\) made from operators and \(\wedge\) only, in which no variables occur twice. A fixed-point term \(\alpha (\gamma_i/x_i : i= 1, \ldots,n)\) is called a Sahlqvist fixed-point term if \(\alpha (x_1, \ldots, x_n)\) is a skeleton and \(\gamma_i\) are either negative fixed-point terms or boxed variables of the form \(f_1^d \cdots f_k^d f\) for \(k < \omega\) and for unary \(f_1, \ldots, f_k \in L\). At last, for a Sahlqvist fixed-point term \(\gamma\), \(\gamma =0\) is called a Sahlqvist fixed-point equation. For a Boolean algebra with operators \(\mathcal{A}\), an \(L\)-term is called conjugated in \(\mathcal{A}\) if it defines a conjugate function in \(\mathcal{A}\). After these definitions, the authors prove the main theorem: Theorem 4.7 {\parindent = 5mm \begin{itemize}\item[(1)] Let \(\mathcal{A}\) be a conjugated fixed-point BAO relative to \(\mathcal{F}\subseteq \mathcal{A}\), and let \((\bar{\mathcal{A}}, \mathcal{F})\) be the completion of \((\mathcal{A}, \mathcal{F})\). Then any Sahlqvist fixed-point equation valid in \(\mathcal{A}\) relative to \(\mathcal{F}\) is also valid in \(\bar{\mathcal{A}}\) relative to \(\mathcal{F}\). \item[(2)] Let \(\mathcal{A}\) be a conjugated BAO and \(\bar{\mathcal{A}}\) its completion. Then any Sahlqvist fixed-point equation valid in \(\mathcal{A}\) is valid in \(\bar{\mathcal{A}}\). \end{itemize}}