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 (B\lor \neg B)}$

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

where ${\displaystyle A}$ and ${\displaystyle B}$ are any propositions. 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[]

Minimal logic is axiomatized over the positive fragment of intuitionistic logic. These logics may be formulated in the language using implication ${\displaystyle \to }$, conjunction ${\displaystyle \land }$ and disjunction ${\displaystyle \lor }$ as the basic connectives, together with the adoption of falsum or absurdity ${\displaystyle \bot }$. Alternatively, direct axioms for negation are discussed below.

Theorems[]

Negations[]

A natural statement in a language with negation, such as Minimal logic, is, for example, the principle of negation introduction, whereby one proves the negation of a statement by assuming it and deriving a contradiction. Formally, this may be expressed as, for any two propositions,

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

For ${\displaystyle B}$ taken as the contradiction ${\displaystyle A\land \neg A}$ itself, this establishes the law of non-contradiction

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

And from just implication introduction and elimination, the above introduction principle implies

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

i.e. assuming any contradiction, every proposition can be negated. Negation introduction is possible in minimal logic, so here a contradiction also proves every double negation ${\displaystyle \neg \neg B}$. Explosion would permit to remove the latter double negation, but this principle is not adopted.

With explosion for negated statements, full explosion is equivalent to its special case ${\displaystyle ((\neg B)\land \neg (\neg B))\to B}$, which can be phrased as double negation elimination for negated propositions, ${\displaystyle \neg B\to (\neg \neg B\to B)}$.

Axiomatization via absurdity[]

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

The already discussed principles can then be established. Negation introduction is implied as a mere special case of

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

when ${\displaystyle C=\bot }$. In this way, minimal logic can be characterized as a constructive logic just without negation elimination (explosion). The above can be proved via modus ponens,

${\displaystyle (A\land (A\to C))\to C}$.

Note that with this definition of negation, modus ponens itself can in the same way again be specialized to the non-contradiction principle ${\displaystyle \neg (A\land \neg A)}$. Moreover, by implication introduction

${\displaystyle C\to (B\to C)}$

and this also already implies ${\displaystyle \bot \to (B\to \bot )}$ showing directly how assuming ${\displaystyle \bot }$ in minimal logic proves all negations, ${\displaystyle \bot \to \neg B}$. If absurdity is primitive, full explosion can also be stated as ${\displaystyle \bot \to B}$.

Going on, minimal logic also proves the contraposition

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

from

${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$.

Double negations[]

In the same way of going from ${\displaystyle \neg B=(B\to \bot )}$ to the more general ${\displaystyle B\to C}$, one can prove

${\displaystyle B\to \neg \neg B}$

from the general ${\displaystyle B\to ((B\to C)\to C)}$. Adopting the contraposition and double negation principles involving "${\displaystyle \neg }$" gives an alternative axiomatization of minimal logic over the positive positive fragment of intuitionistic logic.

Combining the negation from contradiction as well as the double negation formulas, one can see that

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

This is to be compared with the full disjunctive syllogism.

Minimal logic also proves

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

expressing that those are two equivalent ways of the saying that both ${\displaystyle A}$ and ${\displaystyle B}$ are unprovable. Combining this with the contraposition together, we get

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

expressing that those are two equivalent ways of the saying that ${\displaystyle A}$ and ${\displaystyle B}$ cannot both be rejected. Given the validity of the non-contradiction principle, we find

${\displaystyle \neg \neg (B\lor \neg B)}$.

I.e. excluded middle cannot be rejected - for the pure propositional logic.

Unprovable sentences[]

As suggested by all the theorems ending in double negation in the previous section, the tactic of generalizing ${\displaystyle \neg A}$ to ${\displaystyle A\to C}$ does not work to prove all classically valid statements of the form of a double negation. Note that any schema of the syntactic shape ${\displaystyle (A\to C)\to B}$, with ${\displaystyle C}$ and ${\displaystyle B}$ not fixed, is too strong to be provable: If it were provable, then any true proposition ${\displaystyle C}$ would prove any other proposition ${\displaystyle B}$. The particular case of interest with ${\displaystyle A=(B\to C)}$ shows that the naive generalization of the double negation elimination ${\displaystyle \neg \neg B\to B}$ cannot be provable this way.

Naturally, the equivalents of explosion, such as the weak double negation elimination principle ${\displaystyle \neg B\to (\neg \neg B\to B)}$, are not provable in minimal logic either. Adopting it gives intuitionistic logic.

As we have seen, ${\displaystyle \neg \neg (B\lor \neg B)}$ is a theorems of minimal logic, as is ${\displaystyle (A\land \neg A)\to \neg \neg B}$. Therefore, adopting the full double negation principle ${\displaystyle \neg \neg B\to B}$ in minimal logic brings the calculus back to classical logic, also skipping all intermediate logics.

Relation to intuitionistic logic[]

Any formula using only ${\displaystyle \land ,\lor ,\to }$ is provable in minimal logic if and only if it is provable in intuitionistic logic. The principle of explosion is valid in intuitionistic logic and expresses that to derive any proposition, one may do this by deriving an absurdity. In minimal logic, this formula 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.

Formulated concisely, explosion in intuitionistic logic exactly grants particular cases of the double negation elimination principle that minimal logic does not have.

Practically, in the intuitionistic context, the principle of explosion enables the disjunctive syllogism:

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

This can be read as follows: Given a constructive proof of ${\displaystyle A\lor B}$ and constructive rejection of ${\displaystyle A}$, one unconditionally allows for the positive case choice of ${\displaystyle B}$. In this way, it is an unpacking principle for the disjunction. The syllogism can be seen as a formal consequence of explosion and it also implies it. 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, as the system allows for explosion.

In minimal logic, one could not prove ${\displaystyle B}$ this way, but only its double-negation ${\displaystyle \neg \neg B}$. If the minimal logic system is metalogically assumed consistent, then this can be expressed by saying that ${\displaystyle B}$ apriori merely cannot be rejected. If the intuitionistic logic system is metalogically assumed consistent and ${\displaystyle \neg A}$ is established, the full syllogism can be expressed by saying that then a constructive demonstration of ${\displaystyle A\lor B}$ always actually must have come from and contain a proof of ${\displaystyle B}$.

In the other direction, the instance of the disjunctive syllogism with ${\displaystyle A=\neg B}$ reads ${\displaystyle ((B\lor \neg B)\land \neg \neg B)\to B}$ and is equivalent to the double negation elimination for decidable propositions

${\displaystyle (B\lor \neg B)\to (\neg \neg B\to B)}$.

This is again equivalent to double negation elimination for negated propositions.

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 the a family of simple double negation elimination claims, ${\displaystyle \exists }$-sentences binding a computable predicate.

Let ${\displaystyle P}$ be any quantifier-free predicate, and thus decidable for all numbers ${\displaystyle n}$, i.e.

${\displaystyle P(n)\lor \neg P(n)}$.

Then by induction in ${\displaystyle m}$,

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

In words: For the numbers ${\displaystyle n}$ within a finite range up to ${\displaystyle 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 ${\displaystyle n=a}$, the corresponding proposition ${\displaystyle P(a)}$ will always be disprovable, then this implies that we can find some ${\displaystyle n=b}$ among those ${\displaystyle n}$'s for which ${\displaystyle 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 ${\displaystyle m=0}$, then this initial case already gives a form of explosion from a vacuous clause

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

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

${\displaystyle \neg \neg P(0)\to P(0)}$.

The ${\displaystyle m=2}$ case reads

${\displaystyle \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

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

Both ${\displaystyle m=1}$ and ${\displaystyle m=2}$ are again cases of double negation elimination for a decidable predicate. Of course, a statement ${\displaystyle \exists (b<m).P(b)}$ for fixed ${\displaystyle m}$ and ${\displaystyle 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[]

Use of negation[]

Absurdity ${\displaystyle \bot }$ is used not only in natural deduction, but also in 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. The claim of non-existence of a proof for that proposition is then a claim of consistency.

An example characterization for ${\displaystyle \bot }$ is ${\displaystyle 0=1}$ in a theory involving natural numbers. This may also be adopted for in plain constructive logic. With this, proving ${\displaystyle 3^{4}=8}$ to be false, i.e. ${\displaystyle \neg (3^{4}=8)}$, just means to prove ${\displaystyle (3^{4}=8)\to (0=1)}$. We may introduce the notation ${\displaystyle 3^{4}\neq 8}$ to capture the claim as well. 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 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. 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 fewer constraints.

See also[]

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

References[]

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