Minimal logic

Minimal logic is a fragment of intuitionistic logic.

Its syntax consists of propositional atoms and the implication connective (\lnot). Its theorems are those proven by the implication rules of natural deduction.

The main qualitative difference to intuitionistic logic seems to be the lack of an axiom or rule amounting to ex falso quodlibet, viz. \bot \to A.

Axiomatization

Citations are needed for this section.

Minimal logic can be axiomatized by the axioms

• A \to B \to A
• (A \to (B \to C)) \to (A \to B) \to (A \to C)

Notice that these correspond to the types of the \mathbf{K} (kill) and \mathbf{S} (split) combinators.

Natural deduction

A natural deduction system for minimal logic is given by the assumption rule together with introduction and elimination for implication:

\frac{}{\Gamma, A, \Delta \vdash A}
\quad
\frac{
  \Gamma, A \vdash B
}{
  \Gamma \vdash A \to B
}
\quad
\frac{
  \Gamma \vdash A \to B \quad
  \Gamma \vdash A
}{
  \Gamma \vdash B
}

Curry-Howard correspondence

In terms of the Curry-Howard correspondence, minimal logic corresponds to the plain simply-typed \lambda-calculus with \lambda, application, and variables (no products or sums).

References

• Minimal logic was first introduced in

BibTeX

@article{johansson_1937,
	title = {Der {Minimalkalk\"{u}l}, ein reduzierter intuitionistischer {Formalismus}},
	volume = {4},
	journal = {Compositio Mathematica},
	author = {Johansson, Ingebrigt},
	year = {1937},
	pages = {119--136},
}

• There is a Wikipedia page on minimal logic.