Proof theory of Paraconsistent Weak Kleene Logic

Paraconsistent Weak Kleene Logic (PWK) is the 3-valued propositional logic defined on the weak Kleene tables and with two designated values. Most of the existing proof systems for PWK are characterised by the presence of linguistic restrictions on some of their rules. This feature can be seen as a shortcoming. We provide a cut-free calculus (a hybrid between a natural deduction calculus and a sequent calculus) for PWK that is devoid of such provisos. Moreover, we introduce a Priest-style tableaux calculus for PWK.