Semantics of Sequent Calculi with Basic Structural Rules: Fuzziness Versus Non-Multiplicativity

EasyChair Preprint no. 4153

15 pagesDate: September 8, 2020

Abstract

The main  general\/} result of the paper is that
basic\/} structural rules --- Enlargement, Permutation and Contraction ---
(as well as Sharings) [and Cuts] are derivable in
a \{multiplicative\} propositional two-side sequent calculus
iff there is a class of \{crisp\} (reflexive) [transitive distributive] fuzzy two-side
matrices such that any rule is derivable in the calculus iff
it is true in the class,
the \{\}''/()[]''-optional case being
due to \cite{My-label}/\cite{My-fuzzy}.
Likewise, fyzzyfying the notion of signed matrix \cite{My-label},
we extend the main result obtained therein beyond
multiplicative calculi.
As an application, we prove that
the sequent calculus $\mbb{LK}_\mr{[S/C]}$
resulted from Gentzen's $LK$ \cite{Gen}
by adding the rules inverse to the logical ones
and retaining as structural ones merely basic ones
[and Sharing/Cut] is equivalent
(in the sense of \cite{DEAGLS}) to the bounded version of
Belnap's four-valued logic (cf. \cite{Bel})
[resp., the {\em logic of paradox\/} \cite{Priest}/
Kleene's three-valued logic \cite{Kleene}].
As a consequence of this equivalence,
appropriate generic results of \cite{DEAGLS}
concerning extensions of equivalent calculi
and the advanced auxiliary results on extensions of
the bounded versions of Kleene's three-valued logic
and the logic of paradox proved here
with using the generic algebraic tools elaborated in \cite{LP-ext},
we then prove that extensions of the Sharing/Cut-free version
$\mbb{LK}_\mr{C/S}$ of $LK$ form a three/four-element chain/,
consistent ones having same derivable sequents
that provides a new profound insight into Cut Elimination in $LK$
appearing to be just a consequence of the well-known regularity of
operations of Belnap's four-valued logic.

Keyphrases: Calculus, logic, matrix, sequent