Minimal logic

Minimal logic, or minimal calculus, is a symbolic logic system originally developed by Ingebrigt Johansson.[1] 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:

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 one proves the negation of a statement by assuming it and deriving a contradiction. Formally, this may be expressed as, for any two propositions,

The already discussed principles can then be established. Negation introduction is implied as a mere special case of

Closely related to the negation introduction principle, minimal logic also proves the contraposition

Combining the negation from contradiction as well as the double negation formulas, one can see that

I.e. excluded middle cannot be rejected - for the pure propositional logic.

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.

Functional programming calculi already foremostly depend on the implication connective, see e.g. the calculus of constructions for a predicate logic framework.

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:

Each formula of this restricted minimal logic corresponds to a type in the simply typed lambda calculus, see Curry–Howard correspondence.

There are semantics of minimal logic that mirror the frame-semantics of intuitionistic logic, see the discussion of semantics in paraconsistent logic. Here the valuation functions assigning truth and falsity to propositions can be subject to fewer constraints.