Minimal logic is a fragment of intuitionistic logic.
Its syntax consists of propositional atoms and the implication connective (). 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. .
Citations are needed for this section.
Minimal logic can be axiomatized by the axioms
Notice that these correspond to the types of the (kill) and (split) combinators.
A natural deduction system for minimal logic is given by the assumption rule together with introduction and elimination for implication:
In terms of the Curry-Howard correspondence, minimal logic corresponds to the plain simply-typed -calculus with , application, and variables (no products or sums).
Johansson, Ingebrigt. 1937. ‘Der Minimalkalkül, Ein Reduzierter Intuitionistischer Formalismus’. Compositio Mathematica 4: 119–36.
@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},
}