The aim of this paper is to combine several Ivev-like modal systems characterized by 4-valued non-deterministic matrices (Nmatrices) with IDM4, a 4-valued expansion of Belnap-Dunn's logic FDE with an implication introduced by Pynko in 1999. In order to to this, we introduce a new methodology for combining logics which are characterized by means of swap structures, based on what we call superposition of snapshots. In particular, the combination of IDM4 with Tm, the 4-valued Ivlev's version of KT, will be analyzed with more details. From the semantical perspective, the idea is to combine the 4-valued swap structures (Nmatrices) for Tm (and several of its extensions) with the 4-valued twist structure (logical matrix) for IDM4. This superposition produces a universe of 6 snapshots, with 3 of them being designated. The multioperators over the new universe are defined by combining the specifications of the given swap and twist structures. This gives origin to 6 different paradefinite Ivlev-like modal logics, each one of them characterized by a 6-valued Nmatrix, and conservatively extending the original modal logic and IDM4. This important feature allows us to consider the proposed construction as a genuine technique for combining logics. In addition, it is possible to define in the combined logics a classicality operator in the sense of logics of evidence and truth (LETs). A sound and complete Hilbert-style axiomatization is also presented for the 6 combined systems, as well as a very simple Prolog program which implements the swap structures semantics for the 6 systems, which gives a decision procedure for satisfiability, refutability and validity of formulas in these logics.
翻译:本文旨在将几种由四值非确定性矩阵(Nmatrices)刻画的Ivlev式模态系统,与IDM4(Belnap-Dunn逻辑FDE在1999年由Pynko引入一个蕴涵算子后的四值扩张)结合起来。为此,我们引入了一种新方法,用于结合由交换结构刻画的逻辑,其基础是所谓的“快照叠加”(superposition of snapshots)。特别地,我们将详细分析IDM4与Tm(KT的四值Ivlev版本)的结合。从语义角度看,其思想是将Tm(及其若干扩张)的四值交换结构(Nmatrices)与IDM4的四值扭曲结构(逻辑矩阵)相结合。这种叠加产生了一个包含6个快照的论域,其中有3个被指派为指定值。新论域上的多元算子通过结合给定交换结构与扭曲结构的规范来定义。由此产生了6种不同的Paradefinite Ivlev式模态逻辑,每种都由一个六值Nmatrix刻画,并保守扩张了原模态逻辑和IDM4。这一重要特征使我们能够将所提出的构造视为一种真正的逻辑结合技术。此外,在结合逻辑中可以定义证据与真理逻辑(LETs)意义上的经典性算子。我们还为这6个结合系统给出了一个可靠且完备的Hilbert式公理化,以及一个非常简单的Prolog程序,该程序实现了这6个系统的交换结构语义,从而提供了对这些逻辑中公式的可满足性、可反驳性和有效性的判定程序。