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, and therefore holding neither of the following two derivations as valid:
where is any proposition. 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.

Axiomatization

Like intuitionistic logic, minimal logic can be formulated in the language using
an implication,
a conjunction,
a disjunction,
and
falsum or absurdity
as the basic connectives.
Negation is treated as an abbreviation for. Minimal logic is axiomatized as the positive fragment of intuitionistic logic.

Relation to classical logic

Adding the double negation law to minimal logic brings the calculus back to classical logic:
The propositional form of modus ponens,
is clearly valid also in minimal logic.
Constructively, represents a proposition for which there can be no reason to believe it.
To prove propositions of the form, one shows that assuming leads to a contradiction,.
With the principle of explosion this stated as
the principle of explosion expresses that to derive any proposition one may also do this by deriving absurdity. This principle is rejected in minimal logic. This means the formula does not axiomatically hold for arbitrary and.
As minimal logic represents only the positive fragment of intuitionistic logic, it is a subsystem of intuitionistic logic and is strictly weaker.
Practically, this enables the disjunctive syllogism the intuitionistic context:
Given a constructive proof of and constructive rejection of, the principle of explosion unconditionally allows for the positive case choice of.
This is because if was proven by proving then is already proven, while if was proven by proving, then also follows if the system allows for explosion.
Note that with taken for in the modus ponens expression, the law of non-contradiction
i.e., can still be proven in minimal logic.
Moreover, any formula using only is provable in minimal logic if and only if it is provable in intuitionistic logic.

Relation to type theory

Use of negation

Absurdity is necessary in natural deduction, as well as type theoretical formulations under the Curry–Howard correspondence.
In type systems, is often also introduced as the empty type.
In many contexts, need not be a separate constant in the logic but its role can be replaced with any rejected proposition. For example, it can be defined as where ought to be distinct, such as in a theory involving natural numbers.
For example, with the above characterization of, proving to be false, i.e., which is to say proving, just means to prove.
And indeed, using arithmetic, holds, but also implies. So this would imply and hence we obtain. QED.

Simple types

Functional programming calculi 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.
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.

Semantics

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 less constraints.