Preservation of Sahlqvist fixed point equations in completions of relativized fixed point Boolean algebras with operators
type: Item
instance of: scholarly article
title: Preservation of Sahlqvist fixed point equations in completions of relativized fixed point Boolean algebras with operators
zbMATH Open document ID: 1266.06017
author: Nick Bezhanishvili
author: Ian Hodkinson
published in: Algebra Universalis
publication date: 2012-11-27T00:00:00Z
review text: 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 \(\m…
reviewed by: Michiro Kondo
Mathematics Subject Classification ID: 06E25
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03G25
Mathematics Subject Classification ID: 06B23
zbMATH DE Number: 6110491
zbMATH Keywords: modal mu-calculus
zbMATH Keywords: modal mu-algebra
zbMATH Keywords: conjugated operator
zbMATH Keywords: fixed-point equations
zbMATH Keywords: Boolean algebras with operators
MaRDI profile type: Publication
full work available at URL: s00012-012-0196-x
OpenAlex ID: W1986224214
cites work: Q3781066
cites work: Sahlqvist correspondence for modal mu-calculus
cites work: Sahlqvist theorem for modal fixed point logic
cites work: Modal logic
cites work: Q4049062
cites work: MacNeille completions and canonical extensions
cites work: The preservation of Sahlqvist equations in completions of Boolean algebras with operators
cites work: Q5293993
cites work: On the canonicity of Sahlqvist identities
cites work: Boolean Algebras with Operators. Part I
cites work: Completions of B<scp>OOLEAN</scp> Algebras with operators
cites work: A new proof of Sahlqvist's theorem on modal definability and completeness
cites work: Completions of \(\mu \)-algebras
cites work: Q3257817
cites work: MacNeille completions of lattice expansions
DOI: 10.1007/S00012-012-0196-X
Recommended article: The preservation of Sahlqvist equations in completions of Boolean algebras with operators
Recommended article: Q4849832
Recommended article: Sahlqvist preservation for topological fixed-point logic
Recommended article: Sahlqvist's theorem for Boolean algebras with operators with an application to cylindric algebras
Recommended article: A COMPLETENESS RESULT FOR FIXED‐POINT ALGEBRAS
Recommended article: Properties of fixed point operators in predicate algebras
Recommended article: Q4296714
Recommended article: Q4228153
Recommended article: Some propositions equivalent to the Sikorski Extension Theorem for Boolean algebras
Recommended article: Algorithmic Sahlqvist preservation for modal compact Hausdorff spaces
description: scientific article; zbMATH DE number 6110491