Subtractive logic (Q5940919)

From MaRDI portal
Revision as of 21:52, 21 December 2023 by Importer (talk | contribs) (‎Created a new Item)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
scientific article; zbMATH DE number 1635070
Language Label Description Also known as
English
Subtractive logic
scientific article; zbMATH DE number 1635070

    Statements

    Subtractive logic (English)
    0 references
    0 references
    20 August 2001
    0 references
    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.
    0 references
    0 references
    extension of intuitionistic logic
    0 references
    duality
    0 references
    Cartesian closed categories
    0 references
    symmetrical categorical propositional calculus
    0 references
    subtractive logic
    0 references

    Identifiers