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 formula_3 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 formula_3 and formula_8 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 formula_9,
a conjunction formula_10,
a disjunction formula_11,
and
falsum or absurdity formula_12
as the basic connectives. 
Negation formula_8 is treated as an abbreviation for formula_14. Minimal logic is axiomatized as the positive fragment of intuitionistic logic.
Relation to classical logic.
Adding the double negation law formula_15 to minimal logic brings the calculus back to classical logic:
Relation to intuitionistic logic.
The propositional form of modus ponens, 
is clearly valid also in minimal logic.
Constructively, formula_12 represents a proposition for which there can be no reason to believe it. 
To prove propositions of the form formula_8, one shows that assuming formula_3 leads to a contradiction, formula_25.
With the principle of explosion this stated as 
the principle of explosion expresses that to derive any proposition formula_27 one may also do this by deriving absurdity formula_12. This principle is rejected in minimal logic. This means the formula does not axiomatically hold for arbitrary formula_3 and formula_27.
As minimal logic represents only the positive fragment of intuitionistic logic, it is a subsystem of intuitionistic logic and is strictly weaker.
Practically, the principle of explosion enables the disjunctive syllogism the intuitionistic context: 
Given a constructive proof of formula_32 and constructive rejection of formula_3, the principle of explosion unconditionally allows for the positive case choice of formula_27.
This is because if formula_32 was proven by proving formula_27 then formula_27 is already proven, while if formula_32 was proven by proving formula_3, then formula_27 also follows if the system allows for explosion.
Note that with formula_12 taken for formula_27 in the modus ponens expression, the law of non-contradiction 
i.e. formula_44, can still be proven in minimal logic.
Moreover, any formula using only formula_45 is provable in minimal logic if and only if it is provable in intuitionistic logic.
Relation to type theory.
Use of negation.
Absurdity formula_12 is necessary in natural deduction, as well as type theoretical formulations under the Curry–Howard correspondence. 
In type systems, formula_12 is often also introduced as the empty type. 
In many contexts, formula_12 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 formula_49 where formula_50 ought to be distinct, such as formula_51 in a theory involving natural numbers. 
For example, with the above characterization of formula_12, proving formula_53 to be false, i.e. formula_54, which is to say proving formula_55, just means to prove formula_56. 
And indeed, using arithmetic, formula_57 holds, but formula_58 also implies formula_59. So this would imply formula_60 and hence we obtain formula_55. 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 fewer constraints.