Combining swap structures: the case of Paradefinite Ivlev-like modal logics based on FDE

TL;DR

This paper introduces a novel methodology for combining Ivlev-like modal logics with FDE-based logic IDM4 using swap structures, resulting in new 6-valued Ivlev-like modal systems with semantic and axiomatic foundations.

Contribution

It presents a new superposition technique for combining swap and twist structures, creating 6-valued Ivlev-like modal logics with formal semantics and proof systems.

Findings

Six new 6-valued Ivlev-like modal logics are characterized by Nmatrices.

The combined logics extend original modal and IDM4 logics conservatively.

A Hilbert-style axiomatization and a Prolog implementation are provided.

Abstract

The aim of this paper is to combine several Ivlev-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 do 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 rise 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 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 Prolog program which implements the swap structures semantics for the 6 systems, producing a decision procedure for satisfiability, refutability and validity of formulas in these logics.