nLab minimal logic

Idea

Minimal logic [Johansson 1937] is intuitionistic logic without the ex falso quodlibet rule $\bot \vdash A$.

It may also be defined by starting with Gentzen's sequent calculus for classical logic with $\bot$ but not $\neg$, and restricting to sequents $\Gamma \vdash \Delta$ where $\Delta$ must contain exactly one formula. The same is not true if you start with Gentzen's sequent calculus with $\neg$ but not $\bot$; for example, the sequent $p, \neg p \vdash \neg q$ is valid in minimal logic, but it is not derivable in that sequent calculus if each succedent is required to consist of exactly one formula.

Because it is not the case here that anything follows from a falsehood, minimal logic is a paraconsistent logic. However, it still satisfies the weaker law

$$A,\, \neg A \;\vdash\; \neg B$$

for any $A$ and $B$. This is a weaker form of ex contradictione quodlibet, which is still strong enough to be undesirable if one wants to do serious things with a paraconsistent logic.

Categorical semantics of minimal logic is provided by cartesian closed categories, optionally with $n$-ary coproducts for $n\gt 1$.

Under the Curry-Howard correspondence minimal logic corresponds to simply-typed lambda calculus, which, roughly speaking, is another way of saying that both are forms of the internal logic of cartesian closed categories.

 See also

• cartesian closed category

References

The original article:

• Ingebregt Johansson: Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus, Compositio Mathematica 4 (1937) 119-136 [numdam:CM_1937__4__119_0]

Review:

• Sergei P. Odintsov, Chapter 2 in: Constructive Negations and Paraconsistency, Trends in Logic 26, Springer (2008) [doi:10.1007/978-1-4020-6867-6]

See also:

• Wikipedia: Minimal logic