Subtractive logic (Q5940919)

Subtractive logic gets its name from the addition of a ``minus'' binary connective -- to the language of intuitionistic propositional calculus (IPC, with connective symbols \(\top\) (``true''), \(\bot\) (``false''), \(\wedge\) (``and''), \(\vee\) (``or''), and \(\Rightarrow\) (``implies'')). The intended reading for \(p-q\) is ``\(p\), but not \(q\),'' and the symbols \(\top\), \(\wedge\), and \(\Rightarrow\) are respectively ``dual'' to \(\bot\), \(\vee\), and \(-\). The logic of this propositional language arises from the underlying axiomatics of Cartesian closed categories whose category-opposites are also Cartesian closed. \(\top\) and \(\bot\) correspond respectively to the terminal and initial objects; \(\wedge\) and \(\vee\) correspond respectively to the product and coproduct; and \(\Rightarrow\) and \(-\) correspond respectively to the exponent and co-exponent. This symmetrical categorical propositional calculus (SCPC) can be given by a system of axioms and rules, and is shown to be equivalent to the subtractive propositional calculus of \textit{C. Rauszer} [``Semi-Boolean algebras and their applications to intuitionistic logic with dual operations'', Fundam. Math. 83, 219-249 (1974; Zbl 0298.02064)]. The author extends the work of Rauszer with some new facts about subtractive logic, especially non-definability results. He goves on to show that SCPC has a Kripke-style semantics extending that for IPC, and uses this to prove that SCPC is a conservative extension of IPC. In the latter half of the paper, subtractive predicate logic is examined, and found to be a non-conservative extension of intuitionistic predicate logic. A Gentzen-style sequent calculus for this logic is also studied.