Minimal logic

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.

The already discussed principles can then be from theorems over the positive fragment. Negation introduction, spelled out in the previous section, is implied as a mere special case of

Secondly, using it to dissolve one implication from a disjunction as antecedent into two implications, it follows that

Adopting the above double negation principle together with the contraposition principle gives an alternative axiomatization of minimal logic over the positive positive fragment of intuitionistic logic.

As seen above, the double negated excluded middle for any proposition is already provable in minimal logic. However, it is worth emphasizing that in the predicate calculus, the laws of minimal logic do not enable a proof of the double negation of an infinite conjunction of excluded middle statements. Indeed, the double negation shift schema (DNS)

The principle of explosion is valid in intuitionistic logic and expresses that to derive any and all propositions, one may do this by deriving any absurdity. In minimal logic, this principle does not axiomatically hold for arbitrary propositions. As minimal logic represents only the positive fragment of intuitionistic logic, it is a subsystem of intuitionistic logic and is strictly weaker.

Formulated concisely, explosion in intuitionistic logic exactly grants particular cases of the double negation elimination principle that minimal logic does not have.

Practically, in the intuitionistic context, the principle of explosion enables the disjunctive syllogism:

As the material conditional grants double-negation elimination for proven propositions, this is again equivalent to double negation elimination for rejected propositions.

As an aside, the unbounded schema for general decidable predicates is not even intuitionistically provable, see Markov's principle.

In this section we mention the system obtained by restricting minimal logic to implication only, and describe it formally. It can be defined by the following sequent rules: