nLab minimal logic



Minimal logic, introduced by I. Johansson in 1936, is intuitionistic logic without the ex falso quodlibet rule A\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,¬p¬q 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,¬A¬B A,\, \neg A \;\vdash\; \neg B

for any AA and BB. 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.

Models of minimal logic are cartesian closed categories, optionally with finite nn-ary coproducts for n>1n\gt 1. Under the Curry-Howard correspondence minimal logic corresponds to simply-typed lambda calculus, which is roughly speaking another way of saying that both are forms of the internal logic of cartesian closed categories.

 See also


For a definition of the minimal logic, see Chapter 2 in

  • Sergei P. Odintsov?, Constructive Negations and Paraconsistency, Trends in Logic 26, Springer, 2008. doi.

Last revised on July 19, 2023 at 01:08:33. See the history of this page for a list of all contributions to it.