Minimal logic

Minimal logic, or minimal calculus, is a symbolic logic system originally developed by Ingebrigt Johansson. It is an intuitionistic and paraconsistent logic, that rejects both the law of the excluded middle as well as the principle of explosion (ex falso quodlibet), and therefore holding neither of the following two derivations as valid: where and are any propositions. Most constructive logics only reject the former, the law of excluded middle. In classical logic, the ex falso laws as well as their variants with and switched, are equivalent to each other and valid. Minimal logic also rejects those principles. Minimal logic is axiomatized over the positive fragment of intuitionistic logic. Both of these logics may be formulated in the language using the same axioms for implication , conjunction and disjunction as the basic connectives, but Minimal Logic adds falsum or absurdity as part of the language. Alternatively, direct axioms for negation are discussed below. Here only theorems not already provable in the positive calculus are covered. A quick analysis of implication and negation laws gives a good indication of what this logic, lacking full explosion, can and cannot prove. A natural statement in a language with negation, such as Minimal logic, is, for example, the principle of negation introduction, whereby the negation of a statement is proven by assuming it and deriving a contradiction. Formally, this may be expressed as, for any two propositions, For taken as the contradiction itself, this establishes the law of non-contradiction Assuming any , the introduction rule of the material conditional gives , also when and are not relevantly related. With this and implication elimination, the above introduction principle implies i.e. assuming any contradiction, every proposition can be negated. Negation introduction is possible in minimal logic, so here a contradiction moreover proves every double negation . Explosion would permit to remove the latter double negation, but this principle is not adopted.