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 contradiction, minimal logic is 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.


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 January 30, 2021 at 16:17:35. See the history of this page for a list of all contributions to it.