Minimal Logic

Origin. Johansson introduced minimal logic (1937). Weaker than intuitionistic logic. No ex falso quodlibet (⊥ → A not valid). Negation defined: ¬A = A → ⊥, but ⊥ doesn't imply everything. Foundation for studying negation and absurdity.

Models. Implication without explosion. Intuitionistic: ⊥ implies everything (ex falso). Minimal: ⊥ is just a proposition, not special. ¬A = A → ⊥, but from ⊥ alone, can't derive arbitrary B. Relevant to paraconsistency and constructivism.

Formalism.

Axioms (implicational):

1. A → (B → A)
2. (A → (B → C)) → ((A → B) → (A → C))
3. (A → B) → ((A → ¬B) → ¬A)

Where ¬A = A → ⊥.

Compared to intuitionistic: Intuitionistic adds: ⊥ → A (ex falso quodlibet / explosion) Minimal omits this axiom.

Natural deduction: Same rules as intuitionistic, but no ⊥-elimination rule (⊥ ⊢ A).

Key non-theorem: ⊬ ⊥ → A (absurdity doesn't entail everything) ⊬ ¬¬A → A (no double negation elimination, as in intuitionistic)

Negation properties: Minimal: ¬A = A → ⊥, but ⊥ is treated as any other atom. Can have models where ⊥ is true at some worlds.

Extensions:

• Minimal + (⊥ → A) = Intuitionistic
• Intuitionistic + ((A → B) ∨ (B → A)) = Gödel–Dummett LC
• Intuitionistic + (A ∨ ¬A) = Classical

Ex falso must come first. Adding linearity or excluded middle to minimal logic alone gives strictly weaker systems: minimal + (A ∨ ¬A) is not classical logic, since ⊥ → A is still underivable.

Symbols.

Metatheory. Johansson (1937) obtained minimal logic by deleting a single axiom, and almost everything survives the deletion: the disjunction property holds, cut elimination and normalization hold, and derivability is decidable and PSPACE-complete, since the implicational fragment is shared with intuitionistic logic and Statman's lower bound already applies there. The algebraic semantics is Heyting algebras with a distinguished element ⊥ that is not required to be the bottom — contrapositionally complemented lattices — so ¬a := a → ⊥ need not be a pseudocomplement, and the Kripke semantics correspondingly allows an upward-closed set of worlds at which ⊥ holds. Intuitionistic logic is exactly minimal logic plus ex falso, and the two coincide on ⊥-free conclusions from ⊥-free premises: by the subformula property of normal derivations, ⊥ cannot occur in a normal proof that neither begins nor ends with it, so the added axiom is invisible outside the negative fragment. Under Curry–Howard, minimal logic is simply typed lambda calculus with ⊥ as an ordinary type constant and no eliminator for it.

Applies to. Constructive foundations. Negation analysis. Proof theory. Type theory (without empty type elimination). Paraconsistent reasoning. Philosophy of logic.

Limitations. The paraconsistency is only partial, and this is the decisive point: from ⊥ one still derives B → ⊥, that is ¬B, for every B, since weakening is unrestricted. So a contradiction does not entail everything but it does entail the negation of everything, which is enough to trivialize any argument that turns on negative information. Because ⊥ is an ordinary constant, nothing in the syntax marks it as absurd, and a model may satisfy it — in such a model ¬A holds for every A and the negation apparatus says nothing at all. Dropping ex falso also breaks the usual route to classical logic: minimal logic plus excluded middle is not classical, since ⊥ → A remains underivable, so the familiar axiom hierarchy has to be re-derived rather than inherited. And the loss is felt across constructive mathematics, where reasoning by refutation of cases is standard and here unavailable in its intuitionistic form.

© 2026 Lingenic LLC