Non-reflexive Nonsense: Proof-Theory for Paracomplete Weak Kleene Logic

Abstract

Our aim is to provide a sequent calculus whose external consequence relation coincides with the three-valued paracomplete logic `of nonsense´ introduced by Dmitry Bochvar and, independently, presented as the weak Kleene logic K3W by Stephen C. Kleene. The main features of this calculus are (i) that it is non-reflexive, i.e., Identity is not included as an explicit rule (although a restricted form of it with premises is derivable); (ii) that it includes rules where no variable-inclusion conditions are attached; and (iii) that it is hybrid, insofar as it includes both left and right operational introduction as well as elimination rules.