Minimal logic, or minimal calculus, is a symbolic logic system originally developed by Ingebrigt Johansson under the name "". It is a paraconsistent logic weaker than intuitionistic logic that rejects the principle of explosion (ex falso quodlibet), according to which any statement can be proven from a contradiction, as well as the law of the excluded middle. In comparison, intuitionistic logic, like most constructive logics, only rejects the law of excluded middle.
As such, neither of the following two derivations are valid for all propositions and in minimal logic:
, .
In classical logic, also the ex falso law , or equivalently , is valid. These do not automatically hold in minimal logic.
The name minimal logic has sometimes also been used to denote logic systems with a restricted number of connectives.
Syntax and axiomatization Minimal logic is usually formulated using the same syntax as intuitionistic propositional logic, with implication , conjunction , disjunction , and falsum or absurdity as the basic connectives, treating ¬A as an abbreviation for (A → ⊥). Using this syntax, minimal logic has the same axiomatization as the positive fragment of intuitionistic logic, with no axioms that specifically mention .
Alternative formulations of minimal logic with ¬ as a basic connective are possible, so long as explosion is avoided. Such axiomatizations require direct axioms for negation, which are given below. A desideratum is always the negation introduction law, discussed next.
Theorems Negation introduction A quick analysis of the valid rules for negation gives a good preview 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 the negation of a statement is proven by assuming the statement and deriving a contradiction. Over minimal logic, the principle is equivalent to
for any two propositions. For taken as the contradiction itself, this establishes the law of non-contradiction
Assuming any , the introduction rule of the material conditional gives , also when and are not relevantly related. With this and implication elimination, the above introduction principle implies
i.e. assuming any contradiction, every proposition can be negated. With negation introduction possible in this logic, any contradiction proves any double negation. In turn, if is provable for some , then moreover always . Explosion would permit to remove the double negation in the consequents, but this principle is not adopted in minimal logic.
With this, many statements of the form are seen to be equivalent to explosion over minimal logic. To name but one example, .
Axiomatization via absurdity One possible scheme of extending the positive calculus to minimal logic is to treat as an implication, in which case the theorems from the constructive implication calculus of a logic carry over to negation statements. To this end, is introduced as a proposition, not provable unless the system is inconsistent, and negation is then treated as an abbreviation for . Constructively, represents a proposition for which there can be no reason to believe it.
Any implication of the form is equivalent to just . If absurdity is primitive in the logic, the full explosion principle (e.g. in the form with in the above) can thus similarly also be stated as .
What follows are quick arguments showing which theorems still do hold in minimal logic, often making implicit use of the valid currying rule and the deduction theorem.
Implications and negation By implication introduction, , and so by considering , i.e.
Likewise,
may directly be derived from modus ponens in the propositional form . Combining this with the valid contraposition principle (see below), also the stability of negated statements follows,
A second equivalent to follows from Frege's theorem,
This in turn implies a valid weak form of consequentia mirabilis, . In words, this states that a statement cannot be rejected exactly when the negation of the statement implies that it cannot be rejected.
The double-negation introduction entails
and is in turn also entailed by it, as its mere special case when . The rest of this section re-derives the first three theorems above, as a special case of a few other stronger valid theorems, each involving two propositional variables.
Firstly, 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 equivalence is proven there. For a first derivation, setting here at once results in the schema
In the intuitionistic Hilbert system, when not introducing as a constant, this can also be taken as the second negation-characterizing axiom. (The other being explosion.) Now with taken as resp. , the above indeed shows explosion in the form resp. .
Secondly, the double-negation introduction likewise also follows from the mere special case in
which is close to both of the above theorems. The general indeed holds. The special case is itself a generalization of the stability of negated statements. The latter alternatively also follows from . Under the Curry-Howard correspondence, the last theorem here may also be justified by the lambda expression , just to state this method for one of the theorems here.
Thirdly, from contraposition of the implication introduction one has
And similarly entails
From this the double-negation implication follows with as well. Lastly, in minimal logic the contraposition
may be proven from . From this one finds that, for any , one has . So relatedly, this also proves, like negation introduction, that . From these, again, also . The double-negation implication also follows from in using the weak consequentia mirabilis.
Conjunction and disjunction 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 , the modus ponens statement in the form itself specializes to the non-contradiction principle, when considering . When negation is an implication, then the curried form of non-contradiction is again . Further, negation introduction in the form with a conjunction, spelled out in the previous section, is implied as the mere special case of . In this way, minimal logic can be characterized as a constructive logic just without negation elimination (a.k.a. explosion).
With this, most of the common intuitionistic implications involving conjunctions of two propositions can also be obtained, including the currying equivalence. The important equivalence
is worth emphasizing. It expressing that those are two equivalent ways of the saying that both and imply . From it, two of the familiar De Morgan's laws are obtained,
The third valid De Morgan's law may also be derived.
The negation of an excluded middle statement implies its own validity. 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 , which follows from when considering for .
Another, somewhat more specific special case, , already suggests how naive disjunction laws are tied to explosion, a topic discussed in detail further below.
Relatedly, for any , case analysis shows that is equivalent to simply . In particular, is equivalent to . Similarly, is equivalent to . And in particular, is equivalent to , which however is not in general equivalent to just . And now, likewise, salvaged in minimal logic is the implication
This is to be compared with the full, only intuitionistically provable propositional expression of the disjunctive syllogism. Again, only in intuitonistic logic, with explosion, is the consequent here always provably equivalent to just . The disjunctive syllogism as an admissible rule is discussed below.
Intuitionistic logic does not prove , and without one cannot prove the inverse direction either. In turn, not all forms of the resolution rule are valid in minimal logic.
Axiomatization via alternative principles All the above principles can be obtained using theorems from the positive calculus in combination with the constant . Instead of the formulation with that constant, one may adopt as axioms the contraposition principle , together with the double negation principle . This gives an alternative axiomatization of minimal logic over the positive fragment of intuitionistic logic.
Relation to classical logic The tactic of generalizing to does not work to prove all classically valid statements involving double negations. In particular, unsurprisingly, the naive generalization of the double negation elimination cannot be provable in this way. Indeed, whatever looks like, any schema of the syntactic form would be too strong: Considering any true proposition for makes this equivalent to just .
The proposition is a theorem of minimal logic, as is . Therefore, adopting the full double negation principle in minimal logic actually also proves explosion, and so brings the calculus back to classical logic, also skipping all intermediate logics.
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.
Relation to paraconsistent logic Excluded middle is often valid in paraconsistent logics, but not so in minimal logic. In minimal logic, it can be shown to be equivalent to consequentia mirabilis.
Minimal logic only proves the double-negation of excluded middle, and weak variants of consequentia mirabilis, as used above and as shown in its own article.
Relation to relevance logic Minimal logic proves weakening, i.e. allows for implication introduction in the propositional form . That principle plays a role in derivations of deduction theorems.
The law of identity holds even in very weak logics. With it, in minimal logic weakening can further be used to prove .
In, e.g., proving weakening, minimal logic is unlike relevance logic. Hence, of course, the logic discussed here is not minimal in a formal sense.
Relation to intuitionistic logic Any formula using only is provable in minimal logic if and only if it is provable in intuitionistic logic. But there are also propositional logic statements that are unprovable in minimal logic, but do hold intuitionistically.
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. Both logics have the disjunction property.
With explosion for negated statements, full explosion is equivalent to its special case . The latter can be phrased as double negation elimination for rejected propositions, . Formulated concisely, explosion in intuitionistic logic exactly grants particular cases of the double negation elimination principle that minimal logic does not have. This implication also immediately entails the full disjunctive syllogism as in the next section.
Disjunctive syllogism Practically, in the intuitionistic context, the principle of explosion enables proving the disjunctive syllogism in the form of a single proposition: