Self-extensional Paradefinite Four-valued Modal Logic Compatible with Standard Modal Logic

A Gentzen-style sequent calculus GMA4 is introduced for a modal extension MA4 of Avron’s self-extensional paradefinite four-valued logic. A new Gentzen-style sequent calculus GS4
^*
for normal modal logic S4 is obtained from GMA4 by adding two special inference rules. A theorem for equivalence between GS4
^*
and Kripke’s Gentzen-style sequent calculus GS4 for S4 is proved. Cut- and contraposition-elimination theorems for GMA4 and GS4
^*
are proved. The self-extensional properties of GMA4 and GS4
^*
are obtained from the contraposition-elimination theorems.