Minimal logic

Minimal logic, or minimal calculus, is a symbolic logic system originally developed by Ingebrigt Johansson.[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:

${\displaystyle \vdash (A\lor \neg A)}$

${\displaystyle (A\land \neg A)\vdash }$

where ${\displaystyle A}$ is any proposition. Most constructive logics only reject the former, the law of excluded middle. In classical logic, the ex falso laws

${\displaystyle (A\land \neg A)\to B,}$

${\displaystyle \neg (A\lor \neg A)\to B,}$

${\displaystyle A\to (\neg A\to B),}$

as well as their variants with ${\displaystyle A}$ and ${\displaystyle \neg A}$ 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 ${\displaystyle \to }$, a conjunction ${\displaystyle \land }$, a disjunction ${\displaystyle \lor }$, and falsum or absurdity ${\displaystyle \bot }$ as the basic connectives. Negation ${\displaystyle \neg A}$ is treated as an abbreviation for ${\displaystyle A\to \bot }$. Minimal logic is axiomatized as the positive fragment of intuitionistic logic.

Relation to classical logic

Adding the double negation law ${\displaystyle \neg \neg A\to A}$ to minimal logic brings the calculus back to classical logic:

• Excluded middle, ${\displaystyle A\lor \neg A}$, is then the equivalent to the rejection of ${\displaystyle \neg (A\lor \neg A)}$ and is achieved using disjunction introduction on both sides.
• Explosion, ${\displaystyle (A\land \neg A)\to B}$, then follows from proof-by-contradiction ${\displaystyle (C\to (A\land \neg A))\to \neg C}$ using ${\displaystyle C=\neg B}$.

Relation to intuitionistic logic

The propositional form of modus ponens,

${\displaystyle (A\land (A\to B))\to B,}$

is clearly valid also in minimal logic.

Constructively, ${\displaystyle \bot }$ represents a proposition for which there can be no reason to believe it. To prove propositions of the form ${\displaystyle \neg A}$, one shows that assuming ${\displaystyle A}$ leads to a contradiction, ${\displaystyle A\to \bot }$. With the principle of explosion this stated as

${\displaystyle (A\land (A\to \bot ))\to B,}$

the principle of explosion expresses that to derive any proposition ${\displaystyle B}$ one may also do this by deriving absurdity ${\displaystyle \bot }$. This principle is rejected in minimal logic. This means the formula does not axiomatically hold for arbitrary ${\displaystyle A}$ and ${\displaystyle B}$.

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:

${\displaystyle ((A\lor B)\land (A\to \bot ))\to B.}$

Given a constructive proof of ${\displaystyle A\lor B}$ and constructive rejection of ${\displaystyle A}$, the principle of explosion unconditionally allows for the positive case choice of ${\displaystyle B}$. This is because if ${\displaystyle A\lor B}$ was proven by proving ${\displaystyle B}$ then ${\displaystyle B}$ is already proven, while if ${\displaystyle A\lor B}$ was proven by proving ${\displaystyle A}$, then ${\displaystyle B}$ also follows if the system allows for explosion.

Note that with ${\displaystyle \bot }$ taken for ${\displaystyle B}$ in the modus ponens expression, the law of non-contradiction

${\displaystyle (A\land (A\to \bot ))\to \bot ,}$

i.e. ${\displaystyle \neg (A\land \neg A)}$, can still be proven in minimal logic. Moreover, any formula using only ${\displaystyle \land ,\lor ,\to }$ is provable in minimal logic if and only if it is provable in intuitionistic logic.

Relation to type theory

Use of negation

Absurdity ${\displaystyle \bot }$ is necessary in natural deduction, as well as type theoretical formulations under the Curry–Howard correspondence. In type systems, ${\displaystyle \bot }$ is often also introduced as the empty type. In many contexts, ${\displaystyle \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 ${\displaystyle a=b}$ where ${\displaystyle a,b}$ ought to be distinct, such as ${\displaystyle 0=1}$ in a theory involving natural numbers.

For example, with the above characterization of ${\displaystyle \bot }$, proving ${\displaystyle 3^{4}=8}$ to be false, i.e. ${\displaystyle 3^{4}\neq 8}$, which is to say proving ${\displaystyle \neg (3^{4}=8)}$, just means to prove ${\displaystyle (3^{4}=8)\to (0=1)}$. And indeed, using arithmetic, ${\displaystyle {\tfrac {3^{4}-8}{73}}=1}$ holds, but ${\displaystyle (3^{4}=8)}$ also implies ${\displaystyle {\tfrac {3^{4}-8}{73}}=0}$. So this would imply ${\displaystyle 1=0}$ and hence we obtain ${\displaystyle \neg (3^{4}=8)}$. 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:

${\displaystyle {\dfrac {}{\Gamma \cup \{A\}\vdash A}}{\mbox{ axiom}}}$         ${\displaystyle {\dfrac {\Gamma \cup \{A\}\vdash B}{\Gamma \vdash A\to B}}{\mbox{ intro}}}$         ${\displaystyle {\dfrac {\Gamma \vdash A\to B~~~~~~~~~~\Delta \vdash A}{\Gamma \cup \Delta \vdash B}}{\mbox{ elim.}}}$[2][3]

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.

See also

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

References

1. Ingebrigt Johansson (1937). "Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus". Compositio Mathematica (in German). 4: 119–136.
2. M. Weber and M. Simons and C. Lafontaine (1993). The Generic Development Language DEVA: Presentation and Case Studies. LNCS. 738. Springer. p. 246. Here: p.36-40.
3. Gérard Huet (May 1986). Formal Structures for Computation and Deduction. International Summer School on Logic of Programming and Calculi of Discrete Design. Marktoberdorf. Archived from the original on 2014-07-14. Here: p.125, p.132

• A.S. Troelstra and H. Schwichtenberg, 2000, Basic Proof Theory, Cambridge University Press, ISBN 0521779111