Implicational Propositional Calculus

Origin. Frege's Begriffsschrift (1879) already isolates it; Łukasiewicz and Tarski studied the axiomatics through the 1920s–30s; Tarski and Bernays gave the standard three axioms; C. A. Meredith (1953) found a single axiom for the classical fragment. Church's simply typed λ-calculus (1940) is its Curry–Howard image, though nobody said so until Howard (1969).

Models. Classical propositional logic with only →. The fragment is where the axiomatics of implication were worked out, where the substructural weakenings are defined by subtraction, and where Curry–Howard is exact: the intuitionistic implicational calculus and the simply typed λ-calculus are the same object, theorem for type and proof for term.

Formalism.

Positive implicational calculus (intuitionistic): K: A → (B → A) S: (A → (B → C)) → ((A → B) → (A → C)) Rule: modus ponens. Complete for the → -fragment of intuitionistic logic.

Classical: Add Peirce's law: ((A → B) → A) → A K + S + Peirce + MP is complete for the → -fragment of classical logic. Peirce's law is not derivable from K and S — the fragment separates the two logics without needing negation.

Single axiom (Meredith 1953): The classical implicational calculus is axiomatizable by one formula with modus ponens. Łukasiewicz and Meredith produced a series of shortest-known axioms; the enterprise is a curiosity that the automated-reasoning literature later took up seriously.

The substructural ladder — by subtraction: BCK = K + B + C: drops contraction (no W: (A → (A → B)) → (A → B)) BCI = B + C + I: drops weakening as well; the relevant implicational fragment BCK + W = the positive implicational calculus Each combinator is an axiom and each axiom is a structural rule. Curry's combinators and Gentzen's rules are the same list.

Curry–Howard: Intuitionistic implicational calculus ≅ simply typed λ-calculus K ↦ λx.λy.x (the K combinator) S ↦ λx.λy.λz.xz(yz) (the S combinator) MP ↦ application. Normalization ↦ cut elimination.

Functional completeness: → alone is not functionally complete: ¬ and ⊥ are not definable. Adding ⊥ gives the full intuitionistic propositional calculus.

Symbols.

Metatheory. That Peirce's law separates classical from intuitionistic logic inside a fragment with no negation is the fragment's most useful fact: it shows classicality is a property of implication and not of negation, which the ¬¬-elimination framing hides. The combinator correspondence is the second: BCK, BCI, and the positive calculus are the same list as the structural rules, so the substructural hierarchy is visible here before any sequent calculus is written, and Curry saw it in 1930 in the combinators rather than in the logic. The single-axiom results are a genuine curiosity with an afterlife — Meredith's methods and the automated searches that extended them are one of the few places where mechanical proof search found something a human wanted.

Applies to. The axiomatics of implication. Curry–Howard, in its cleanest instance. The substructural hierarchy, defined by which combinators are available. Automated reasoning, where single-axiom problems are a benchmark. Any argument that separates classical from intuitionistic reasoning without negation.

Limitations. Not functionally complete, so it is a fragment and not a logic anyone reasons in — everything interesting needs ⊥ or ¬ added back. The single-axiom literature is a sport: the axioms are unreadable and prove nothing the three-axiom presentation does not. And the fragment's tractability is deceptive: the decision problem is still PSPACE-complete for intuitionistic implication, and coNP-complete for classical.

© 2026 Lingenic LLC