次协调式Nelson逻辑的模态扩展及其代数完备性证明

可在www.sciencedirect.com在线获取理论计算机科学电子笔记278（2011）173-186www.elsevier.com/locate/entcs次协调模态逻辑UmbertoRivieccio综合科学日本科学技术高级研究所Nomi，日本摘要本文介绍了次协调Nelson逻辑的一种模态扩展，它也是Odintsov和Wansing最近提出的Belnapian模态逻辑的推广。我们证明了这两个逻辑的代数完备性定理，定义和公理化相应的代数语义。我们给出了这些代数的扭结构表示，推广了关于次协调Nelson逻辑代数对应物表示的一个已知结果.关键词：次协调模态逻辑，纳尔逊逻辑，扭结构，贝尔纳普逻辑。1引言非经典逻辑研究的最新和最具挑战性的趋势之一是试图将不同的非经典方法结合在一起，例如多值逻辑和模态逻辑[14]，[15]。这种相互作用有利于处理模态概念，如信念，知识，义务，以及可以使用多值逻辑最好地处理的推理的其他方面，例如不一致性[18]，[6]和不一致性。如果目标是对人类推理进行建模，那么显然必须同时处理所有这些方面，因此从理论计算机科学和人工智能的角度来看，这种研究特别有趣。最著名的逻辑系统之一是处理不一致和部分信息的Belnap-Dunn逻辑[13]，[3]，[4]。这个系统基于四个真值，可以认为是两个经典的真值加上两个附加值，分别表示缺乏信息和不一致性（见贝尔纳普提出的著名解释[3]）。这种简单的方法，后来由Ginsberg [17]用双格的概念推广，被证明是非常简单的。1电子邮件：rUmberto@jaist.ac.jp1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.10.014174联合Rivieccio/理论计算机科学电子笔记278（2011）173它具有灵活性，在计算机科学的各个领域都有广泛的应用。在[25]中，Odintsov和Wansing提出了Belnap-Dunn逻辑的模态扩展，旨在将Belnap的方法扩展 在目前的工作中，我们继续在这条线上的研究，但采取更一般的方法，引入一个逻辑，可以被视为一个概括的Odintsov和Wansing的。我们的主要目的是介绍一个模态扩展的Belnap-Dunn逻辑，这是某种程度上最小的（在某种意义上，将在下面精确）和研究这个系统的代数逻辑工具。这样，我们得到了Odintsov和Wansing的一些本文的结构如下。在第二节中，我们介绍了次协调纳尔逊逻辑，这是一个非模态系统，我们将建立我们的次协调模态逻辑。我们用代数术语重新表述了这个逻辑的完备性定理，这将使我们能够为我们将要介绍的模态展开获得类似的完备性结果。在第3节中，我们介绍了我们的模态版本的次协调纳尔逊逻辑。我们看到，[25]的贝尔纳潘模态我们展示了如何将这些结果应用于任何扩展（即，加强）的上述逻辑;我们介绍和公理化类代数，为他们提供代数语义。在第4节中，我们证明了这些代数的表示定理，推广了已知的表示结果的代数对应的次协调纳尔逊逻辑。最后，在第5节中，我们提到了一些开放的问题和未来研究的可能路线。2纳尔逊逻辑我们首先回顾了关于次协调Nelson逻辑[2]的一些已知结果，这是我们将作为构建基础的非模态系统模态逻辑 我们的选择是出于这样一个事实，即在这种逻辑中，有可能将贝尔纳普的方法与不完整/不一致的数据相结合，具有相当强的蕴涵连接，它基本上具有直觉蕴涵的所有属性。纳尔逊逻辑的模态展开已经在文献中考虑过，例如在[23]，[24]和[29]中（见第3节）。其他的选择当然也是可能的，例如，人们可以像[26]那样在贝尔纳普-邓恩逻辑中加入经典（而不是直觉主义）蕴涵（然而，这个逻辑的模态对应物可以很容易地作为我们的公理化加强而获得定义2.1次协调纳尔逊逻辑N4 =<$Fm，<$N4<$是语言{k，k，k，<$}中的逻辑，由希尔伯特式演算定义，公理联合Rivieccio/理论计算机科学电子笔记278（2011）173175示意图：（1）p（qp）（2）（p（qr））（（pq）（pr））（）（pq）p（pq）q（）（pq）（（pr）（p（qr））（）p（pq）q（pq）（p r）（（qr）（（pq）r）（q）（q）（<$）<$（pq）（p<$q）（<$$>）p<$p其中，假设前件推理（MP）是唯一的推理规则：ppqQ纳尔逊逻辑N3 =<$Fm，<$N3<$通过将以下公理加到N4上得到：（<$$>）<$p<$（p<$q）。在N3中，通常考虑另一个一元连接词，称为直觉否定（−），与强否定（<$）相对。 直觉主义否定可以用强否定来定义如下：-：= ϕ⊃ 好吧我们还将使用以下缩写： ϕ→ ψ ：=（ ） ⊃ <$）和Participant：=（→）（→）。不难证明N4是Belnap-Dunn逻辑的保守扩展（例如参见[16]中给出的公理表示），即，这两个逻辑的推论关系在无条件公式上是一致的下面是另一个有趣的比较（对我们的目标更有用注2.2正如在[20，p.456]中所观察到的，定义2.1的公理， 不涉及强否定构成了正逻辑的公理化[28]，{，，}- 直觉主义逻辑的因此，任何在正逻辑在N4中也是有效的。我们将使用这个事实作为引理来缩短我们的证明。Odintsov [20]证明了次协调Nelson逻辑N4对于一类称为N4-格的代数是完备的，定义如下[20，定义5.1]。定义2.3一个N4-格是一个代数A=<$A，<$A，<$A，<$A，<$A使得：(i) 约简子A，A，B，C是德摩根格，即，一个分配格，配备有一元运算a= a和b，对于所有a，b ∈ A，(ii) 对于所有a，b∈A，关系≤定义为a≤bi <$a<$b=（a<$b）<$（a<$b），是预序（即，反应性和传递性），176联合Rivieccio/理论计算机科学电子笔记278（2011）1732∈H 联 系我们⟨H.H.(iii) 对于所有的a，b∈A，定义为a∈b i ∈ a≤b且b≤a的关系是关于r. t的同余关系。并且商代数A，A/A是Brouwerian格，(iv) 对于所有的a，b∈A， <$（ab）a<$b，(v) 对所有的a，b∈A，a≤bi ∈a≤b且<$b≤<$a，其中≤是A.称A是有界的，如果它的格约简是有界的。A称为N3-格3如果它是N4-晶格， 对所有a，b∈A，<$a≤a<$b。N4-格形成一个簇[20，定理6.3]，我们用N4 Lat表示。这个类也可以表示为各种剩余格（参见[8]），其剩余对是（x，→），其中运 算 x定 义 为x y：=<$（x →<$y）。N4-格是次协调Nelson逻辑的代数语义（在[5，定义2.2]的意义上）。为了正式陈述这个结果，让我们定义一个从公式（用次协调纳尔逊逻辑的语言）到公式对的翻译τ：Fm→Fm×Fm（即， 公式），如下：对于所有τ∈Fm，τ（τ）：=.这以明显的方式扩展到任何ΓFm也就是说， τ（Γ）：={τ（τ）：τ∈ Γ}。 让我们在等式的推论中用N4Lat表示关系（定义见[5，p.13]）由类N4Lat确定。我们有以下内容：定理2.4对任意的Γ<${<$}<$Fm，Γ <$N4<$i<$τ（Γ）<$N 4 Latτ（τ）。事实上，很容易证明N4Lat是次协调Nelson逻辑的等价代数语义[5，定义2.8]。为了证明这一点，我们定义了一个逆平移ρ：Fm×Fm→Fm，它对N4-格语言中的任何方程赋予公式ρ（）：=Participate。作为[20，引理6.9]的直接结果，得到了下面的结果定理2.5对任意的ε，ε∈Fm，ϕ≈ ψ =||= N4LatParticipants（Participants）（Participants）.将定理的陈述改写如下：ϕ≈ψ =||= N4Latτ·ρ（πππ）我们立即得到：2一个布劳威尔格是一个格L，配备了一个二元运算，满足以下条件：对于所有a，b，c L，a b c当且仅当b a c。Brouwerian格正是Heyting代数的0-free子约;它们在文献中也被称为广义Heyting代数[10]、Brouwerian代数[12]、关联格[20]或相对伪补格[28]。还请注意，有些作者称之为[3]例如，在[27]和[32]中研究的N-格N-格是通过向N4-格的语言添加额外的一元运算符（对应于直觉否定）而获得的（与我们的N3-格不同，它们是严格地说，不是N4-格的子变种联合Rivieccio/理论计算机科学电子笔记278（2011）173177定理2.6次协调Nelson逻辑N4可代数化. 具有等价公式<$Participant和定义方程<$Participant的N4-格簇。作为推论，我们得到关于N3的如下已知结果（见[30]）推论2.7纳尔逊逻辑N3可代数化w.r.t. 具有等价公式<$Participant和定义方程<$Participant的N3-格簇。3模态纳尔逊逻辑我们现在要介绍和研究我们的模态版本的（次协调）纳尔逊逻辑。我们从逻辑的语法定义开始，然后寻找适当的代数语义。如上所述，我们选择逻辑的标准是定义一个尽可能一般的系统（包括[25]中作为特例考虑的所有贝尔纳潘模态逻辑），但从代数的角度来看仍然表现良好。事实上，在下面的定义中引入的逻辑在某种程度上是最小的，因为如果想要得到像定理3.6那样的代数完备性结果，就需要像（Q1）和（Q2）这样的规则（尽管它们可以被削弱，正如我们将看到的）。定义3.1ModalN4是语言{k，k，k，k，Q}中的逻辑MN4=kFm，kMN4k，由定义（Q1）pqQpQq（Q2）q<$Qp <$<$Qq.模态N3是MN4的公理化扩展，通过添加公理N，（pq）。注意，MN4的结果关系是全局关系，在这个意义上，它是通过将规则（而不仅仅是公理）添加到其非模态基础上获得的。我们将使用以下缩写：Q：=<$Q<$。我们对Q反应的定义 假设强否定有一个几乎经典的行为（如发生在非模态纳尔逊逻辑）也关于模态。这样的假设等价于[24]（也见[23]和[29]）中称为形式对偶的性质，其中表明存在Nelson逻辑的自然模态展开，这些展开式既不强于MN 4也不弱于MN4，因为它们满足了在我们的逻辑中失败的附加公理。这种逻辑和我们的逻辑之间的关系的研究构成了一个有趣的问题，为未来的研究。另一方面，在[25]中引入的贝尔纳潘模态逻辑BK可以被看作是MN4的语言扩展（和公理化加强）。BK语言是通过在MN4语言上增加一个伪常数而得到的。BK可以通过在我们的表示中添加以下公理来公理化[25，定理4178联合Rivieccio/理论计算机科学电子笔记278（2011）173MN4：（3）（（pq）p）p（）（中文）(K1)（Qp<$Qq）<$Q（p<$q）(K2)Q（pp）（−Q）−Qp<$Q−p（−Q）−Qp<$Q−p其中-。让我们注意到，前三个公理（K3），（K1）和（K2）确保了语言{K1，K2，K3，K4，K5}中经典非模态逻辑的所有定理也是BK的定理，而（K1）和（K2）告诉我们，BK是一个（多值）正规模态逻辑。 最后两个公理显然涉及两个模态与两个否定的相互作用（回想一下，Q在定义上是<$Q<$），但是当我们考虑BK的代数对应物时，它们的意义将变得更加清楚。在[25]中，BK的一些公理扩展被引入作为经典模态逻辑的著名系统的Belnapian对应部分，例如：B 3 K ：= BK +<$p（pq）BS 4：= BK +{Qpp，QpQQp} B3 S 4：= B3 K +{Qpp，QpQQp}.我们的下一个目标是获得MN4的代数完备性定理（以及作为推论的MN4的所有扩展/扩展）。我们将需要以下引理。引理3.2对于一个集合，f∈Fm，F参与者MN4Q参与者Q。证据使用注释2.2，很容易证明公式Participant在N 4中（因此，更有理由在MN4中）与公式集合Γ ={Participant，Participant，<$Participant，<$Participant}是可互导的。因此，为了证明该引理，证明如下是足够的：ΓMN4QQ，ΓMN4Q Q，ΓMN4<$Q<$<$Q，ΓMN4你好你好前两个推导很容易遵循规则（Q1），而对于后两个我们应用（Q2）。Q[5，定理4.7]的一个简单的结论是，通过向可代数化逻辑（即，N4）也是代数可化的（具有相同的平移），只要新的连接词满足[5，定理4.7]的项（iv），这对应于我们的引理3.2。同样的推理也适用于BK及其扩展，因为这些逻辑是从MN4中只增加一个常数（显然满足[5，定理4.7（iv）]）和公理而得到的。因此，我们立即有以下内容：联合Rivieccio/理论计算机科学电子笔记278（2011）173179定理3.3逻辑MN 4和BK（以及这两个逻辑的所有扩展）都可以用等价公式<$Participate和定义方程<$Participate代数化。我们现在要定义一个代数，证明它是MN4和BK的等价代数语义。定义3.4一个MN 4-格是一个代数A=A，A，B，C，<$，<$，Q<$，使得约简A，A，B，C，C，<$，<$是一个N4-格，并且对于所有的a，b∈A，(Q1)如果a≤b，则Qa≤Qb(Q2)如果 a≤b，则 <$Qa≤<$Qb。按照逻辑所采用的符号，我们写Qa作为<$Q<$a的简写。定义3.5 BK-格是一个代数A=A，A，B，C，<$，<$，Q，<$，使得约简A，A，B，C，C，<$，Q<$是一个MN 4-格，其中有一个区别元素<$∈A，并且对所有a，b∈A，(E1)（a）a≤a(E2)<$=<$<$(E3)≤a(E4)Qa<$Qb≤Q（a<$b）(E5)Q（aa）=Q（aa）<$Q（aa）(E6)−Qa<$Q−a(E7)−Qa<$Q−a其中ab表示两个等式a≤b和b≤a，而−a表示一个小女孩。很容易检查我们的BK-格与[22]中引入的那些格一致，以提供逻辑BK的代数语义（这是从定理3.6以及[22]第5节末证明的结果得出的）。注意，在前面的定义中，（E2）和（E3）可以等价地替换为假设A的格约简是有界的（底部和顶部元素分别是和）。上面的代数类，我们用MN4Lat和BKLat表示，通过定义是拟簇（我们将证明BKLat实际上是一个簇）。读者可能已经注意到，定义3.4和3.5通过简单地将我们的平移τ应用于模态公理而获得，MN4和BK的规则。这个过程是由Blok和Pigozzi [5，定理2.17]引入的，作为公理化任何可代数化逻辑的等价代数语义的算法。因此，考虑到定理2.6，下面的结果是直接的。定理3.6 MN 4是可代数化的。MN 4-格的类MN 4Lat，BK是可 代数化的。B K -格的类BKLat。从[5，推论4.9]可以得出，MN4和BK的所有扩张，180联合Rivieccio/理论计算机科学电子笔记278（2011）173特别是在[25]中考虑的那些（即，B3K，BS4和B3S4）也是代数化的.BK-格的子拟簇，可以通过添加附加公理和规则的τ-平移来公理化。在下一节中，我们将使用由扭结构表示给出的MN 4-格的更具体的描述来提供关于这些代数类的4MN 4-格的表示一些与非经典逻辑相关的代数（不仅是N4-格，还有双格[7]和一些剩余格[31]）的一个有趣的特征是它们可以用所谓的扭曲结构表示。这种表示非常方便，因为它允许通过处理更传统和更知名的结构（如布尔代数或海廷代数）来解决有关这些代数的许多问题。另一个优点是，扭曲结构构造可以用于引入新的代数（和相应的逻辑），同时共享一些期望的特征，例如，布尔代数，适合于次协调推理（例如见[19]）。众所周知，N3-格可以通过扭曲结构来表示（例如参见[32]），而对于N4-格，Odintsov [20]最近已经获得了这样的结果。在本节中，我们将看到如何扩展Odintsov设L=L，H，H，\n为Brouwerian格（定义见脚注2）。L上的全扭结构是一个代数Lda=<$L×L，<$，其中对所有<$a1，a2<$，<$b1，b2<$∈L×L定义运算如下：a1，a2a1，a2a1，a2<$a1，a2<$：=<$a2，a1<$。L上的扭结构是一个子代数A（w.r.t.到语言{，<$}）的完全扭结构Lda使得π1（A）=L，其中π1（A）={a1∈L：a2<$a1，a2<$∈A}.我们现在可以注意到，“扭转结构”这个名字每个二进制运算的第一个分量被定义为直积，而第二个分量则以某种方式扭曲。很容易检验任何扭结构都是N4-格。对所有的A，a1，a2<$，b1，b2<$∈A，给出了格序：a1，a2<$≤b1，b2<$i <$a1±b1和b2±a2，其中±是Brouwerian格L的格序.因此，通过假设π1（A）=L，我们得到，如果A是有界的，那么它的底元素是0，1，顶元素是1，0，其中0和1分别是L的底元素和顶元素。回想一下，根据定义2.3（iii），对于任何N4-格A=<$A，商代数<$A，B是布劳威尔格让一个人：=A，联合Rivieccio/理论计算机科学电子笔记278（2011）173181如下定理4.1任何N4-格A通过映射i：A→ A/A/A/A/A同构于A上的扭结构，定义为i（a）：= A [a]，[<$a] A，其中[a]表示a∈A模A的等价类。我们的下一个目标是获得类似的结果MN 4-格。为此，我们将扩展扭结构构造如下。给定一个具有相关阶±的格L，我们说函数f：L→L是L上的模态算子，如果它是单调的，即，如果a±b蕴涵f（a）±f（b），则对所有a，b∈L.定义4.2设L=L，H，H，l，f，g是具有模态算子f，g的Brouwerian格。代数Lda=<$L×L，n，n，n，Q定义如下：(i) 约化的L×L，H，H，H，H上的全扭结构(ii) 对于所有的a1，a2∈L×L，运算Q：L×L→L×L被定义为：Q<$a1，a2<$：=<$f（a1），g（a2）<$.注意，f和g之间的交互作用没有要求。例如，可能发生f=g。我们的构造显然是[25，定义7]中引入的构造的推广（并受到其启发）。事实上，如果我们增加额外的要求，即L是一个模态布尔代数4，那么我们精确地获得Odintsov和Wansing命题4.3对于任何具有模态算子L= L的Brouwerian格，如果L，H，H，I，f，g是一个MN 4-格，则 在 定 义 4.2 中 构 造 的代数Lda是一个MN 4-格。证据 从[20，命题5.2]中我们知道Lda的{，，<$，<$}-约简是一个N4-格。只需检查定义3.4的（Q1）和（Q2）是否满足。通过[20，命题5.2（a）]，我们有，对所有的<$a1，a2<$，<$b1，b2 <$∈L×L，<$a1，a2<$≤<$b1，b2<$i <$a1±b1，其中±是L的格序.因此，如果a1，a2<$≤由f的单调性得到f（a1）± f（b1），它等价于Q<$a1，a2<$≤ Q<$b1，b2<$. 类似的论证，利用g的单调性，表明（Q2）也是满足的。Q命题4.4设A = A，Q，A是一个MN 4-格。然后又道：(i) 根据定义2.3（iii）的关系式与运算Q和Q相容(ii) 商代数A<$=<$A，<$，Q，Q<$/<$是具有模态算子Q和Q的Brouwerian格。证据（i）.与Q的兼容性直接从（Q1）开始。Q的情况也很容易用（Q2）证明。（二）. 根据定义2.3（iii），商代数A，A，A，A，A/A是Brouwerian4 模态布尔代数或简单模态代数[9]是一个代数<$L，H，H，\，f，g，0， 1<$，使得约简L，H，H，\，0，1是一个布尔代数，对所有的a，b ∈ L，其模态算子满足：f（aH b）= f（a）Hf（b），f（1）=1和f（a）=g（a′）′，其中a′表示a（可定义为a\0）的布尔补.182联合Rivieccio/理论计算机科学电子笔记278（2011）173晶格只剩下检查Q和Q的单调性。由定理4.1和[20，命题5.2（a）]，我们知道，对于所有a，b∈A， a≤b等价于[a]±[b]，其中±是商格的格序A，如果[a] ± [b]，则a≤b，由（Q1）表示Qa≤Qb。后者，使用了与Q相容的事实，意味着[Qa]=Q[a]±Q[b]=[Qb]。Q的单调性可以用同样的方法证明Q定理4.5任何MN 4-格A同构于A上的扭结构，如定义4.2所定义，通过由i（a）：=<$[ a ]，[<$a ]<$给出的映射i：A→A/<$×A/<$，对于所有a∈ A。证据由定理4.1可知，映射ι是对应的N4-格约简之间的同构。只需要检查i是关于Q的同态，即，对于所有a∈A，i（Qa）=QJi（a），其中QJ表示根据定义4.2（ii）在扭结构上定义的运算。我们有：i（Qa）=<$[Qa]，[<$Qa]<$=a]由双重否定律=[Qa]，[Q<$a]由定义=<$Q[a]，Q[<$a]由命题4.4表示=Qj[a]，[<$a]=QJi（a）。Q利用上面的代数结果，我们现在可以更精确地计算在引言中提到的MN 4的正如我们在第3节中所看到的，从[5，定理4.7]可以得出，次协调Nelson逻辑的最弱可代数化扩展（只有一个基本模态Q）是通过将引理3.2的规则添加到次协调Nelson逻辑的任何公理表示中获得的：Participation（一）然而，很容易检查具有根据定义4.2构造的算子的Brouwerian格上的任何扭结构，即使我们放弃对算子的任何要求（在我们的情况下，单调性），也将满足以下条件：(i)如果a≠b，则Qa≠Qb，（ii）如果<$a≠ <$b，则<$Qa≠ <$Qb。在一个合乎逻辑的级别，这些对应于规则：普什克QpQqpQq它们明显强于（1），但仍略弱于定义3.1中用来引入我们的逻辑MN4的那些。我们现在将使用定理4.5来获得更多关于BK-格的信息，并比较定义给出的这类代数的抽象表示3.5与[25，定义7]中介绍的基于扭结构的一个。联合Rivieccio/理论计算机科学电子笔记278（2011）173183设A是一个MN 4-格。通过定理4.5，我们可以假设A是其关联Brouwerian格上的扭结构，其中模态算子L=L，H，H，f，g，即，AμL×L。 假设有一个元素a1，a2∈A，满足-是 定 义 3.5 中 的 （ E2 ） 和 （ E3 ） 。 然 后 ， 通 过 （ E2 ） ， 我 们 有 <$a2 ，a1<$=<$$>a1，a2<$=a2，a1因此，a2= 1。 (E3)告诉我们，对于任意的∈A，我们有a1±b1，其中±是L的格序。π1（A）=L的假设允许我们得出结论，a1是L的底元素（我们用0表示），因此，a1，a2<$=<$0，1 <$。然后我们看到，（E2）和（E3）正好对应于A的格约简有界（在这种情况下，相关的Brouwerian晶格也有界，即，它实际上是一个Heyting代数）。以类似的方式，很容易检查（E1）成立当且仅当相关的布劳威尔格L满足皮尔士这样的代数被称为广义布尔代数[1]或经典关联格[11]，对应于布尔代数的0-自由子约简。因此，（E1）、（E2）和（E3）合起来成立当且仅当L是布尔代数。(E6) 和（E7）是定义L=L，H，H，l，f，g中两个模态算子相互作用的恒等式。例如，（E6）的一个实例是−Q≤Q−，这意味着f（a1）J±g（aJ1），其中J：L→L是布尔补运算。与（E7）一起，这意味着这两个模态算子可以用经典的方式相互定义。所以，（E1）到（E7）合起来说L是一个模态布尔代数。从这些考虑中，立即得出以下结果。定理4.6任何BK-格（定义见定义3.5）同构于模布尔代数上的扭结构， 定 义 见[25，定义7]。前面的结果可以很容易地被扩展以获得对应于Odintsov和Wansing的逻辑BS 4的BK-格类另外满足Qa±a和QQa=Qa）的模态代数现在我们将使用定理4.6来证明作为拟簇（定义3.4和3.5）引入的BK-格类实际上是一个簇。我们需要以下引理。引理4.7任何BK-格都满足下面的方程：Q（x<$y）≤Qx<$Qy（2）证据 利用BK-格的扭结构表示和[20，Proposition[5.2（a）]，我们很容易看出证明（2）相当于检查，在任何模态布尔代数B中，对于所有a，b ∈ B，它保持f（a\b）± f（a）\f（b）。 通过留数，我们得到前一不等式等价于f（a）H f（a\b）± f（b）. 回想一下，任何布尔代数（事实上，甚至任何布劳威尔格）都满足xH（x\y）= xHy。现在我们利用方程f（x H y）= f（x）H f（y）得到f（a）H f（a\b）= f（a H（a\b））= f（aH b）= f（a）H f（b）± f（b），从而结束我们的证明.Q184联合Rivieccio/理论计算机科学电子笔记278（2011）173我们现在能够证明BK-格是等式可公理化的，即，它们形成了一个变种。引理4.8设A=A，Q，A是一个代数，使得是N4-格，并且满足以下等式(i) (E1)定义3.5的（E7）(ii) （2）引理4.7。则定义3.4的准方程（Q1）和（Q2）也满足，即，A是 一个BK格。证据 为了证明A满足（Q1），设a，b∈A使得a≤b，即， ab=（ab）（ab）。通过（E5），这意味着Q（a<$b）= Q（a<$b）<$Q（a<$b）。应用（2），我们得到Q（a<$b）<$Q（a<$b）≤Qa<$Qb。回想一下，在任何N4-格中，对于所有的a，b，a≠a≤b意味着b=b≠b（这可以很容易地使用N4-格的扭曲结构表示因此，我 们 得 到Qa<$Qb= （ Qa<$Qb ） <$ （ Qa<$Qb ） ， 即 ， Qa≤Qb 。为 了 证 明（Q2），我们将使用以下性质：a≤bi −b≤ −a（同样，使用扭结构表示，可以很容易地检查这在任何有界N4-格中都成立）。假设<$a≤<$b，即， − <$b≤−<$a。 应用（Q1），我们得到Q− <$b≤Q− <$a。由（E7），我们有−Q<$b≤ Q−<$b≤Q− <$a≤−Q<$a。因此，根据所以，我们得到-Q<$b≤-Q<$a。 如上所述，这意味着Q-a≤Q-b，即，a≤b。现在，应用双重否定律，我们得到<$Qa≤ <$Qb。Q引理4.7和4.8直接暗示了预期的结果。定理4.9 BK-格的类是一个簇，由定义N4-格的簇加上定义3.5的（E1）-（E7）和引理4.7的（2）的方程公理化。注意，在引理4.8的证明中，只使用了（E5）和（E7），这意味着具有N4-格约简并满足引理4.7的这两个等式加上（2）的代数类也是一个簇。一个有趣的问题（仍然没有解决）是MN 4-格类是否也是等式可公理化的。在下一节中，我们将提到一些更开放的问题和进一步的研究路线。5结论和今后的工作前面几节给出的结果显然只是对Nelson（和Belnapian）逻辑的模态展开的初步例如，我们只处理了与这些逻辑相关联的全局后果关系。这样的选择使我们能够得到代数完备性结果，作为逻辑代数化的一般理论的直接应用;然而，模态逻辑中通常考虑的后果概念下一步是研究与我们的逻辑相关的局部结果;这与找到一个适当的联合Rivieccio/理论计算机科学电子笔记278（2011）173185可能世界语义（这可能是一个邻域语义，因为我们的逻辑是非正规的），就像Odintsov和Wansing在[25]中为BK所做的如上所述，有模态扩展的次协调纳尔逊逻辑，是不可比的逻辑在本文中介绍。这表明，定义次协调Nelson逻辑的最小模态展开的问题还没有完全普遍地解决。一个相关的问题是，确定这样的逻辑是否可以被赋予一个代数语义，admits某种扭曲结构表示。这些问题将在今后的出版物中讨论。在我们看来，另一个有趣的问题是，我们的方法是否可以通过考虑非模态片段比次协调纳尔逊逻辑弱的系统来进一步推广，例如，具有像某些子结构（而不是直觉主义）逻辑那样的蕴涵的逻辑。这个问题也许可以用代数的方法来解决，扩展了[19] 用于定义剩余晶格上的扭曲结构。最后，我们认为，从纯代数的角度来看，MN 4-格也值得进一步研究。一个有趣的问题是，定理4.5给出的MN 4-格的表示是否可以通过给出全扭曲结构的哪些子集对应于MN 4-格的宇宙的特征来加以改进（参见[21，定理3.1]和[22，第6节]，其中解决了N4-格和BK-格的类似问题引用[1] 阿巴德，M.，波士顿警局。Varela和A. Torrens，Topological representation for implicationsalgebras，Algebra Universalis52（2004），pp. 39比48[2] Almukdad，A.和D. Nelson，Constructible false and inexact predicates，The Journal of SymbolicLogic49（1984），pp. 231-233[3] 贝尔纳普，N. D、计算机应该如何思考，在：G。赖尔，编辑，《当代哲学》，Oriel出版社，波士顿，1976年。30比56[4] 小贝尔纳普N. D、一个有用的四值逻辑，在：J.M. Dunn和G. Epstein，编辑，现代用途多值逻辑（第五国际）Sympos.，印第安纳大学，印第安纳州布卢明顿，1975），Reidel，Dordrecht，1977，pp. 5-37Episteme，Vol.二、[5] Blok，W. J.和D. Pigozzi，普罗维登斯，1989年。[6] Bou，F.，F. 埃斯特湖 G odo和R. R od r'ıguez，关于有限剩余格上的最小多值模型，逻辑与计算杂志（2011年）。[7] Bou，F.，R. Jansana和U.Rivieccio，Varieties of interlaced bilattices，Algebra Universalis.[8] 布萨尼切湾和R.Cignoli，Residuated lattices as an algebraic semantics for paraconsistentNelson1019-1029[9] Chagrov，A.和M. Zakharyaschev，[10] 西尼奥利河和A.满足方程的Glivenko MTL-代数簇中的Torrens2（x2）=（2x）2，Studia Logica83（2006），pp. 157-181。[11] 库里，H。B、《数学逻辑基础》，多佛出版公司，纽约，1977年，viii+408页，更正重印。186联合Rivieccio/理论计算机科学电子笔记278（2011）173NN[12] 戴维湾，澳-地一、 Dualities for equational classes of Brouwerian algebras and Heyting algebras，Transactions of the Americal Mathematical Society 221（1976），pp. 119-146[13] Dunn，J.M.， D. 匹兹堡大学论文（1966年）。[14] Fitting，M.，多值模态逻辑，Fundamenta Informaticae15（1992），pp. 235-254。[15] Fitting，M.，多值模态逻辑，II，Fundamenta Informaticae17（1992），pp.55比73[16] 丰特，J.M.，贝尔纳普5（1997），pp. 413-440[17] Ginsberg，M. L.，Multivalued logics：A uniform approach to inference in arti ficial intelligence，Computational Intelligence4（1988）.265-316[18] 哈 杰 克 山 口和 D.Harmanc ov'a， Amany-valueddmodallogic ， in ： ProceedingsIPMU'96.InformationProcessing and Management of Uncertainty in Knowledge-Based Systems，格拉纳达大学，格拉纳达，1996年，页。1021-1024[19] 扬萨纳河和联合Rivieccio，Residuated bilattices，Soft Computing，2011，DOI 10.1007/s00500-011-0752-x.[20] Odintsov，S. P.，次协调纳尔逊逻辑的代数语义453-468[21] Odintsov，S. P.， 关于N4-格的表示，Studia Logica76（2004），pp. 385-405[22] Odintsov，S. P和E. I.拉特金BK格子贝尔纳潘模态逻辑的代数语义学，Mandarin。[23] Odintsov，S. P.和H. Wansing，Inconsistency-tolerant description logic：motivation and basic systems，V. Hendricks and J. Malinowski，editors，50 Years of Studia Logica，Kluwer，Dordrecht，2003，pp.301-335.[24] Odintsov，S. P.和H. Wansing，构造谓词逻辑和构造模态逻辑。形式的二元性与语义的二元性，在：V.亨德里克斯等人，编辑，First-Order Logic Revisited，Logos Verlag，Berlin，2004 pp. 269-286。[25] Odintsov，S. P.和H. Wansing，模态逻辑与Belnapian真值，应用非经典逻辑杂志20（2010），pp。279-301[26] Pynko，A.P.，贝尔纳普四值逻辑及其扩展中的功能完备性和公理化性61比105[27]Rasiowa，H.，- 格和强否定的构造性逻辑，数学基础46（1958），pp. 61比80[28] Rasiowa，H.，“An algebraic approach to non-classical logics,” Studies in Logic and the Foundations ofMathematics[29] Sherkhonov，E.，构造性逻辑上的模态算子，Journal of Logic and Computation18（2008），pp. 815-829[30] Spinks，M.和R.Vero，强否定的构造逻辑是一种亚结构逻辑，Studia Logica，88（2008），pp. 325-348[31] 茨纳基斯角 和A. M. Wille，对合剩余格的极小簇，Studia Logica83（2006），pp. 407-423[32] Vakarelov ， D. ， Notes on -lattices and constructive logic with strong negation ， Studia Logica36（1977）， pp. 109比125