Proof theory of paraconsistent weak Kleene logic (Q2193974)

Paraconsistent Weak Kleene logic (\(\mathbf{PKW}\)) is the three-valued logic that arises from the weak truth-tables due to \textit{S. C. Kleene} [Introduction to metamathematics. Groningen: P. Noordhoff N. V. (1952; Zbl 0047.00703)], where the intermediate value is taken to be a designated value. Until very recently, (\(\mathbf{PKW}\)) has been the little brother of the other logics in the Kleene family in terms of recognition by the logical and philosophical communities. In [\textit{D. E. Szmuc}, Log. Log. Philos. 28, No. 2, 277--330 (2019; Zbl 1452.03070)] it was already noted that there has been a revival of interest for (\(\mathbf{PKW}\)), both from a semantic and from a proof-theoretic point of view. In the present paper, it is noted that on the proof-theoretic side, many of the presented calculi have some linguistic restrictions on some of their rules. A calculus is provided that avoid such side conditions. The presented calculus is somewhere in between a sequent calculus and a natural deduction calculus. Furthermore, a Priest-style tableau calculus for (\(\mathbf{PKW}\)) that uses signed formulas, is introduced.