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
Minimal + ((A → B) ∨ (B → A)) = Gödel-Dummett
Minimal + A ∨ ¬A = Classical

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. Disjunction property fails (unlike intuitionistic). Kripke models: like intuitionistic but ⊥ can be true at worlds. Weaker than intuitionistic, stronger than positive logic. Complete for algebraic semantics (lattices with pseudocomplement operation).

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. Disjunction property lost. Specialized use cases. Most constructive math uses intuitionistic.