Contents (This is a stub) Idea Subtractive logic is an extension of (propositional or first order) intuitionistic logic with a new connective, subtraction, dual to implication, such that each sentence have a “dual” verifying if and only if . Propositional subtractive logic is a conservative extension over propositional intuitionistic logic, but it is not the case for the first order case. Syntax In the following and to the rest of the articles, uppercases letters will denote sentences. We start with (a slightly modified) Gentzen's LJ sequent calculus, whose rules are as follow: Axioms: Cut: Rules of conjonctions: Rules of disjonctions: Rules of implications: This rule usually do not have a dual in intuitionistic logic, but we’ll just create one written , rules of subtractions: Giving the syntax of propositional subtractive logic, to make it first order, it suffice to add the existential operator and its dual, the forall operator (where does not occur free in ): and Definition The dual of a sentence is another sentence defined by structural induction on the syntax of the sentence by
Relation to other logics (this is a stub) TODO: bi-interpretation with classical logic, what becomes when there’s the law of excluded middle, conservation over propositional intuitionistic logic but not over first order one. Models and semantics (this is a stub) TODO: bi-topologies (where closed sets are also a topology) as models, category semantics of bi-cartesian closed categories, kripke semantics References: