Algebraic semantics of the $\left\{ \rightarrow , \square \right\} $-fragment of Propositional Lax Logic
Algebraic semantics of the $\left\{ \rightarrow , \square \right\} $-fragment of Propositional Lax Logic
复制标题
命题宽松逻辑的 $left{ ightarrow , square ight} $ 片段的代数语义
DOI：
10.1007/s00500-019-04536-9
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
D. Montangie
中科院分区：
文献类型：
--
作者：
S. Celani;D. Montangie
在本文中，我们将使用模态算子研究希尔伯特代数的一个特定子类型，称为 Lax 希尔伯特代数。这些代数是特定直觉模态逻辑片段的代数语义，称为命题宽松逻辑（），它可应用于计算机硬件的形式验证。这些代数变成了由 Macnab (Algebra Univ 12:5–29, 1981)、Goldblatt (Math Logic Q 27(31–35):495–529, 1981; J Logic Comput 21(6):1035–1063, 以不同名称研究的各种 Heyting 代数的推广，其中包括模态算子。 2010）以及 Bezhanishvili 和 Ghilardi （Ann Pure Appl Logic 147：84-100，2007）。我们将证明 Lax Hilbert 代数的不动点集是一个 Hilbert 代数，使得它的对偶空间同胚于 A 的对偶空间的自反元素子空间。我们将定义希尔伯特空间子框架的概念，并证明 和二元关系的子框架之间存在 1-1 对应关系，因此是一个宽松的希尔伯特空间。此外，我们将定义子架簇的概念，并证明任何希尔伯特代数簇都是子架簇。
In this paper, we will study a particular subvariety of Hilbert algebras with a modal operator, called Lax Hilbert algebras. These algebras are the algebraic semantic of the-fragment of a particular intuitionistic modal logic, calledPropositional Lax Logic(), which has applications to the formal verification of computer hardware. These algebras turn to be a generalization of the variety of Heyting algebras with a modal operator studied, under different names, by Macnab (Algebra Univ 12:5–29, 1981), Goldblatt (Math Logic Q 27(31–35):495–529, 1981; J Logic Comput 21(6):1035–1063, 2010) and by Bezhanishvili and Ghilardi (Ann Pure Appl Logic 147:84–100, 2007). We shall prove that the set of fixpoints of a Lax Hilbert algebrais a Hilbert algebra such that its dual space is homeomorphic to the subspace of reflexive elements of the dual space ofA. We will define the notion of subframe of a Hilbert space, and we will prove that there is a 1–1 correspondence between subframes ofand binary relationssuch thatis a Lax Hilbert space. In addition, we will define the notion of subframe variety and we will prove that any variety of Hilbert algebras is a subframe variety.