[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: where
Note that the name has sometimes also been used to denote logic systems with a restricted number of connectives.
as the basic connectives, but minimal logic conventionally adds falsum or absurdity
A quick analysis of the valid rules for negation gives a good preview of what this logic, lacking full explosion, can and cannot prove.
With this and implication elimination, the above introduction principle implies i.e. assuming any contradiction, every proposition can be negated.
One possible scheme of extending the positive calculus to minimal logic is to treat
It may be expressed as If absurdity is primitive, full explosion principle could likewise also be stated as
As for the adopted principles in the implication calculus, which do not involve negations, the page on Hilbert system presents it through propositional forms of the axioms of law of identity, implication introduction and a variant of modus ponens.
, the above shows that But, secondly, this short implication may also more directly be derived from modus ponens in the propositional form
Going beyond statements solely in terms of implications, the principles discussed previously can now also be established as theorems: With the definition of negation through
Further, negation introduction in the form with a conjunction, spelled out in the previous section, is implied as the mere special case of
With this, most of the common intuitionistic implications involving conjunctions of two propositions can be obtained, including the currying equivalence.
With reference to the weak variant of consequentia mirabilis above, it thus follows that This result may also be seen as a special case of
Finally, case analysis shows This implication is to be compared with the full disjunctive syllogism, discussed in detail below.
does not work to prove all classically valid statements involving double negations.
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, not even the laws of the strictly stronger intuitionistic logic enable a proof of the double negation of an infinite conjunction of excluded middle statements.
Indeed, In turn, the double negation shift schema (DNS) is not valid either, that is Beyond arithmetic, this unprovability allows for the axiomatization of non-classical theories.
Minimal logic proves weaker variants of consequentia mirabilis, as demonstrated in that article.
Practically, in the intuitionistic context, the principle of explosion enables the disjunctive syllogism: This can be read as follows: Given a constructive proof of
For example, given a constructive argument that a coin flip resulted in either heads or tails (
If the intuitionistic logic system is metalogically assumed consistent, the syllogism may be read as saying that a constructive demonstration of
If the minimal logic system is metalogically assumed consistent, then that implication formula can be expressed by saying that
The following Heyting arithmetic theorem allows for proofs of existence claims that cannot be proven, by means of this general result, without the explosion principle.
The result is essentially a family of simple double negation elimination claims,
As with examples discussed previously, a proof of this requires explosion on the antecedent side to obtain propositions without negations.
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.
Here the valuation functions assigning truth and falsity to propositions can be subject to fewer constraints.