A syntactical study of the subminimal logic with Nelson negation (Q2479743)

The subminimal logic, SUBMIN-N, is a propositional calculus with two negations, \(\neg\) and (Nelson negation) \(\sim\). It was investigated by \textit{D. Vakarelov} [Stud. Log. 80, No. 2--3, 393--430 (2005; Zbl 1086.03026)] with the goal of weakening the intuitionistic negation as much as possible. On the other hand, \(\sim\) is strong. Indeed \(\sim\sim\!A\) and \(\sim\!\neg A\) are both equivalent to \(A\). Vakarelov's method is model-theoretic, whereas the author carries out a proof-theoretic investigation in this paper. A sequent calculus for SUBMIN-N is formulated, and, of course, the cut-elimination theorem is proved. From it follow, as usual, interpolation theorems and the disjunction property. Howeyer, SUBMIN-N lacks the following three properties -- ``counter-intuitively'' one might say: \((\neg)\) there is a provable formula of the form \(\neg A\), \((\supset)\) if \(A\supset B\) is provable and \(A\) and \(B\) have no common propositional letter, then either \(\neg A\) or \(B\) is provable, and (N) the calculus is normalizable, i.e., it is finitely axiomatizable by schemes in such a way that each axiom has, besides \(\supset\), at most one connective. The author extends the calculus by adding a new axiom \(\neg\neg T\) or \(\neg T\supset A\) or both, obtaining MIN-N, CO-MIN-N and INT-N, respectively. Again, cut-elimination etc. are proved. As to the above three properties, INT-N has them all, MIN-N lacks (N) but has the other two, and CO-MIN-N has none of them.