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):

A → (B → A)
(A → (B → C)) → ((A → B) → (A → C))
(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.

Symbol	Unicode	Name	Meaning
→	U+2192	Implication	If-then
⊥	U+22A5	Absurdity	Falsum
¬	U+00AC	Negation	A → ⊥
∧	U+2227	Conjunction	And
∨	U+2228	Disjunction	Or
⊢	U+22A2	Proves	Derivability

Metatheory. Minimal logic decidable. The disjunction property holds, as in intuitionistic logic — dropping ex falso does not cost it. Kripke models: like intuitionistic but ⊥ can be true at worlds. Weaker than intuitionistic, stronger than positive logic. Algebraic semantics: 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.

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

Limitations. Less common than intuitionistic. Ex falso sometimes desired. Limited tool support. Reasoning from a contradiction is blocked, which is the point but also the cost. Specialized use cases. Most constructive math uses intuitionistic.