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:

$\vdash (B\lor \neg B)$

$(A\land \neg A)\vdash$

where $A$ and $B$ are any propositions. Most constructive logics only reject the former, the law of excluded middle. In classical logic, also the ex falso law

$(A\land \neg A)\to B$,

or equivalently $\neg A\to (A\to B)$, is valid. These do not automatically hold in minimal logic.

Note that the name minimal logic sometimes also been used to denote logic systems with a restricted number of connectives.

Axiomatization

Minimal logic is axiomatized over the positive fragment of intuitionistic logic. Both of these logics may be formulated in the language using the same axioms for implication $\to$, conjunction $\land$ and disjunction $\lor$ as the basic connectives, but minimal logic conventionally adds falsum or absurdity $\bot$ as part of the language.

Other formulations are possible, of course all avoiding explosion. Direct axioms for negation 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

$(B\to (A\land \neg A))\to \neg B$,

for any two propositions. For $B$ taken as the contradiction $A\land \neg A$ itself, this establishes the law of non-contradiction

$\neg (A\land \neg A)$.

Assuming any $C$, the introduction rule of the material conditional gives $B\to C$, also when $B$ and $C$ are not relevantly related. With this and implication elimination, the above introduction principle implies

$(A\land \neg A)\to \neg B$,

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 $\neg C$ is provable for some $C$, then moreover always $C\to \neg \neg B$. 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 $C\to B$ also seen equivalent to explosion, over minimal logic. To name but one example, $\neg (A\lor \neg A)\to B$.

Axiomatization via absurdity

One possible scheme of extending the positive calculus to minimal logic is to treat $\neg B$ as an implication, in which case the theorems from the constructive implication calculus of a logic carry over to negation statements. To this end, $\bot$ is introduced as a proposition, not provable unless the system is inconsistent, and negation $\neg B$ is then treated as an abbreviation for $B\to \bot$. Constructively, $\bot$ represents a proposition for which there can be no reason to believe it.

Any implication of the form $(A\to C)\to (A\to B)$ is equivalent to just $C\to B$. If absurdity is primitive in the logic, the full explosion principle (e.g. in the form with $C=\bot$ in the above) can thus similarly also be stated as $\bot \to B$.

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, $C\to (B\to C)$, and so $\bot \to (B\to \bot )$ by considering $C=\bot$, i.e.

$\bot \to \neg B$.

Likewise,

$B\to \neg \neg B$

may directly be derived from modus ponens in the propositional form $B\to ((B\to C)\to C)$. Combining this with the valid contraposition principle (see below), also the stability of negated statements follows,

$\neg \neg \neg B\leftrightarrow \neg B$.

A second equivalent to $\neg B$ follows from Frege's theorem,

$(B\to \neg B)\leftrightarrow \neg B$.

This in turn implies a valid weak form of consequentia mirabilis, $(\neg B\to \neg \neg B)\leftrightarrow \neg \neg B$. 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 in turn is entailed by, the mere special case $B=\neg \neg A$ in

• ${\big (}\neg \neg A\to B{\big )}\to {\big (}A\to B{\big )}$

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. Note the equivalence ${\big (}B\to (A\to C){\big )}\leftrightarrow {\big (}A\to (B\to C){\big )}$ proven there. For a first derivation, setting $C=\bot$ here at once results in the schema

• ${\big (}B\to \neg A{\big )}\leftrightarrow {\big (}A\to \neg B{\big )}$

In the intuitionistic Hilbert system, when not introducing $\bot$ as a constant, this can also be taken as the second negation-characterizing axiom. (The other being explosion.) Now with $A$ taken as $\bot$ resp. $\neg B$, the above indeed shows explosion in the form $\bot \to \neg B$ resp. $B\to \neg \neg B$.

Secondly, the double-negation introduction likewise also follows from the mere special case $B=\neg A$ in

• ${\big (}\neg \neg A\to \neg B{\big )}\leftrightarrow {\big (}A\to \neg B{\big )}$

which is close to both of the above theorems. The general ${\big (}([A\to C]\to C)\to (B\to C){\big )}\leftrightarrow {\big (}A\to (B\to C){\big )}$ indeed holds. The special case ${\big (}[(B\to C)\to C]\to C{\big )}\leftrightarrow (B\to C)$ is itself a generalization of the stability of negated statements. The latter alternatively also follows from ${\big (}[(B\to C)\to C]\to D{\big )}\to (B\to D)$. Under the Curry-Howard correspondence, the last theorem here may also be justified by the lambda expression $\lambda f^{((B\to C)\to C)\to D}.\ \lambda b^{B}.\ f(\lambda g^{B\to C}.g(b))$, just to state this method for one of the theorems here.

Thirdly, from $A\to {\big (}B\leftrightarrow (A\to B){\big )}$ and contrapositions, one has

• ${\big (}\neg (A\to B){\big )}\to {\big (}A\to \neg B{\big )}$

This entails ${\big (}\neg \neg (A\to B){\big )}\to {\big (}A\to \neg \neg B{\big )}$, from which the double-negation implication follows with $B=A$, also.

Lastly, in minimal logic the contraposition

• $(B\to A)\to (\neg A\to \neg B)$

may be proven from $(B\to A)\to ((A\to C)\to (B\to C))$. From this one finds that, for any $B$, one has $A\to (\neg A\to \neg B)$. So relatedly, this also proves, like negation introduction, that $(A\land \neg A)\to \neg B$. From these, again, also $\bot \to \neg B$. The double-negation implication also follows from $B=\neg A$ in $A\to (\neg A\to \neg B)$ 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 $\bot$, the modus ponens statement in the form $(A\land (A\to C))\to C$ itself specializes to the non-contradiction principle, when considering $C=\bot$. When negation is an implication, then the curried form of non-contradiction is again $A\to \neg \neg A$. Further, negation introduction in the form with a conjunction, spelled out in the previous section, is implied as the mere special case of ${\big (}B\to (A\land (A\to C)){\big )}\to (B\to C)$. 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

${\big (}(A\lor B)\to C{\big )}\leftrightarrow {\big (}(A\to C)\land (B\to C){\big )}$

is worth emphasizing. It expressing that those are two equivalent ways of the saying that both $A$ and $B$ imply $C$. From it, two of the familiar De Morgan's laws are obtained,

$\neg (A\lor B)\leftrightarrow (\neg A\land \neg B)$.

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

$\neg \neg (B\lor \neg B)$

This result may also be seen as a special case of ${\big (}(B\lor (B\to C))\to C{\big )}\to C$, which follows from $((A\lor B)\to C)\to (B\to C)$ when considering $B\to C$ for $A$.

Another, somewhat more specific special case, ${\big (}(A\lor \bot )\to A{\big )}\leftrightarrow (\bot \to A)$, already suggests how naive disjunction laws are tied to explosion, a topic discussed in detail further below.

Relatedly, for any $A$, case analysis shows that $(B\lor A)\land (A\to B)$ is equivalent to simply $B$. In particular, $(B\lor \neg B)\land (\neg B\to B)$ is equivalent to $B$. Now in intuitonistic logic, even $(B\lor \neg B)\land (\neg B\to \bot )$ is equivalent to $B$, but proof of the forward direction of this depends a case of explosion. What can be salvaged in minimal logic is

${\big (}(B\lor \neg A)\land \neg \neg A{\big )}\to {\big (}(B\lor \neg B)\land \neg \neg B){\big )}$

This implication is to be compared with the full, only intuitionistically provable propositional expression of the disjunctive syllogism.

Axiomatization via alternative principles

All the above principles can be obtained using theorems from the positive calculus in combination with the constant $\bot$. Instead of the formulation with that constant, one may adopt as axioms the contraposition principle $(B\to A)\to (\neg A\to \neg B)$, together with the double negation principle $B\to \neg \neg B$. This gives an alternative axiomatization of minimal logic over the positive fragment of intuitionistic logic.

Relation to classical logic

The tactic of generalizing $\neg A$ to $A\to C$ does not work to prove all classically valid statements involving double negations. In particular, unsurprisingly, the naive generalization of the double negation elimination $\neg \neg B\to B$ cannot be provable in this way. Indeed whatever $A$ looks like, any schema of the syntactic form $(A\to C)\to B$ would be too strong: Considering any true proposition for $C$ makes this equivalent to just $B$.

The proposition $\neg \neg (B\lor \neg B)$ is a theorem of minimal logic, as is $(A\land \neg A)\to \neg \neg B$. Therefore, adopting the full double negation principle $\neg \neg B\to B$ 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,

$\nvdash \neg \neg \forall (n\in {\mathbb {N} }).Q(n)\lor \neg Q(n)$

In turn, the double negation shift schema (DNS) is not valid either, that is

$\nvdash {\big (}\forall (n\in {\mathbb {N} }).\neg \neg P(n){\big )}\to \neg \neg \forall (n\in {\mathbb {N} }).P(n)$

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 $C\to (B\to C)$. That principle plays a role in derivations of deduction theorems.

The law of identity $A\to A$ holds even in very weak logics. With it, in minimal logic weakening can further be used to prove $B\to (A\to A)$.

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 $\land ,\lor ,\to$ 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 $((\neg B)\land \neg (\neg B))\to B$. The latter can be phrased as double negation elimination for rejected propositions, $\neg B\to (\neg \neg B\to B)$. 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:

$((A\lor B)\land \neg A)\to B.$

This can be read as follows: Given a constructive proof of $A\lor B$ and constructive rejection of $A$, one unconditionally allows for the positive case choice of $B$, and here not only the double-negation thereof. In this way, the syllogism is an unpacking principle for the disjunction. It can be seen as a formal consequence of explosion and it also implies it. This is because if $A\lor B$ was proven by proving $B$ then $B$ is already proven, while if $A\lor B$ was proven by proving $A$, then $B$ also follows, as the intuitionistic system allows for explosion.

For example, given a constructive argument that a coin flip resulted in either heads or tails ($A$ or $B$), together with a constructive argument that the outcome was in fact not heads, the proposition encapsulating the syllogism expresses that then this already constitutes an argument that tails occurred.

If the intuitionistic logic system is metalogically assumed consistent, the syllogism may be read as saying that a constructive demonstration of $A\lor B$ and $\neg A$, in the absence of other non-logical axioms demonstrating $B$, actually contains a demonstration of $B$.

Johansson proves in his article that even if $((A\lor B)\land \neg A)\to B$ is not a theorem of minimal logic, from the provability of $(A\lor B)\land \neg A$, the provability of $B$ follows. Thus, this step is what is called an admissible rule of inference. His proof uses Gentzen's sequent calculus for intuitionistic logic.

Weak forms of explosion prove the disjunctive syllogism and in the other direction, the instance of the syllogism with $A=\neg B$ reads ${\big (}(B\lor \neg B)\land \neg \neg B{\big )}\to B$ and is equivalent to the double negation elimination for propositions for which excluded middle holds

$(B\lor \neg B)\to (\neg \neg B\to B)$.

As the material conditional grants double-negation elimination for proven propositions, this is again equivalent to double negation elimination for rejected propositions.

Finally, note that with explosion, in intuitionistic logic $A\lor (\bot \to P)$ holds trivially for any $A$. E.g., this disjunction is intuitionistically also provable for $A=\bot$, a false disjunct (which itself is not provable even in classical logic). Minimal logic in general does not prove either the two disjuncts.

Intuitionist example of use in a theory

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, $\exists$-sentences binding a computable predicate.

Let $P$ be any quantifier-free predicate, and thus decidable for all numbers $n$, so that excluded middle holds,

$P(n)\lor \neg P(n)$.

Then by induction in $m$,

$\forall m.\ \neg {\big (}\forall (n<m).\neg P(n){\big )}\to \exists (b<m).P(b)$

In words: For the numbers $n$ within a finite range up to $m$, if it can be ruled out that no case is validating, i.e. if it can be ruled out that for every number, say $n=a$, the corresponding proposition $P(a)$ will always be disprovable, then this implies that there is some $n=b$ among those $n$'s for which $P(b)$ is provable.

As with examples discussed previously, a proof of this requires explosion on the antecedent side to obtain propositions without negations. If the proposition is formulated as starting at $m=0$, then this initial case already gives a form of explosion from a vacuous clause

$\bot \to \exists (b<0).P(b)$.

The next case $m=1$ states the double negation elimination for a decidable predicate,

$\neg \neg P(0)\to P(0)$.

The $m=2$ case reads

$\neg {\big (}\neg P(0)\land \neg P(1){\big )}\to {\big (}P(0)\lor P(1){\big )}$,

which, as already noted, is equivalent to

$\neg \neg {\big (}P(0)\lor P(1){\big )}\to {\big (}P(0)\lor P(1){\big )}$.

Both $m=0$ and $m=1$ are again cases of double negation elimination for a decidable predicate. Of course, a statement $\exists (b<m).P(b)$ for fixed $m$ and $P$ may be provable by other means, using principles of minimal logic.

As an aside, the unbounded schema for general decidable predicates is not even intuitionistically provable, see Markov's principle.

Relation to type theory

Simple types

In this section we mention the system obtained by restricting minimal logic to implication only. Functional programming calculi already foremostly depend on the implication connective, see e.g. the calculus of constructions for a predicate logic framework.

The system can be defined by the following sequent rules:

${\dfrac {}{\Gamma \cup \{A\}\vdash A}}{\mbox{ axiom}}$         ${\dfrac {\Gamma \cup \{A\}\vdash B}{\Gamma \vdash A\to B}}{\mbox{ intro}}$         ${\dfrac {\Gamma \vdash A\to B~~~~~~~~~~\Delta \vdash A}{\Gamma \cup \Delta \vdash B}}{\mbox{ elim.}}$

Each formula of this restricted minimal logic corresponds to a type in the simply typed lambda calculus, see Curry–Howard correspondence. This implicational fragment of minimal logic is the same as the positive, implicational fragment of intuitionistic logic and, in the type theory context, often also already denoted as "minimal logic".

Use of negation

Absurdity $\bot$ is used not only in natural deduction, but also in type theoretical formulations under Curry–Howard. In type systems, $\bot$ is often also introduced as the empty type. The existence of a proof for that proposition then constitutes an inconsistency.

Arithmetic

In many contexts, $\bot$ 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 $a=b$ where $a,b$ ought to be distinct. That proposition may then by denoted by the same symbol, $\bot$. Such a definition may also be fruitful over plain constructive logic.

An example characterization for such $\bot$ is $0=1$ in a theory involving natural numbers. Note that assuming $\bot$ here, any two given numbers can be proven equal. For example, with $1=0$ follows $7=6+1=6+0=6$. Also note that a proof of this form is possible also in absence of Explosion, the logical axiom. An arithmetic is hence dubbed inconsistent if $0=1$ can be derived.

In a context with this definition, proving $3^{4}=8$ to be false, i.e. $\neg (3^{4}=8)$, just means to prove $(3^{4}=8)\to (0=1)$. We may introduce the notation $3^{4}\neq 8$ to capture the claim as well. And indeed, using arithmetic, ${\tfrac {3^{4}-8}{73}}=1$ holds, but $(3^{4}=8)$ also implies ${\tfrac {3^{4}-8}{73}}=0$. So this would imply $1=0$ and hence we obtain $\neg (3^{4}=8)$. QED.

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.

See also

• Intuitionistic logic
• Paraconsistent logic
• Implicational propositional calculus
• List of logic systems

References

• Colacito, Almudena (2016). Minimal and Subminimal Logic of Negation (PDF). MSc Thesis (Afstudeerscriptie). Institute for Logic, Language and Computation.
• Huet, Gérard (May 1986). Formal Structures for Computation and Deduction. International Summer School on Logic of Programming and Calculi of Discrete Design. Archived from the original on 2014-07-14.
• Johansson, Ingebrigt (1937). "Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus". Compositio Mathematica (in German). 4: 119–136.
• Sørensen, Morten Heine B.; Urzyczyn, Paweł [in Polish] (May 1998). "Lectures on the Curry-Howard Isomorphism" (PDF).
• Troelstra, Anne Sjerp; Schwichtenberg, Helmut (2003) [1996]. Basic Proof Theory (2 ed.). Cambridge University Press. pp. XII, 417. ISBN 9780521779111.
• Weber, Matthias; Simons, Martin; Lafontaine, Christine (1993). The Generic Development Language Deva: Presentation and Case Studies. Lecture Notes in Computer Science (LNCS). Vol. 738. Springer. p. 246. ISBN 3-540-57335-6.