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; Łukasiewicz found a single axiom for the classical fragment and proved it shortest (1948). 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 (Łukasiewicz 1948): 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 linear implicational fragment BCIW = B + C + I + W: contraction back, weakening still absent; the relevant implicational fragment R→ BCK + W = BCKW = 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 {→, ⊥} fragment, in which ¬A := A → ⊥ is available — but not the full intuitionistic propositional calculus: ∧ and ∨ are not intuitionistically definable from → and ⊥ and must be taken as primitive. (Classically they are definable, so {→, ⊥} is functionally complete for classical logic.)

Symbols.

Metatheory. K and S with modus ponens are complete for the implicational fragment of intuitionistic logic, and adding Peirce's law gives completeness for the classical fragment. Peirce's law is independent of K and S, so classicality is a property of implication and not of negation, which the ¬¬-elimination framing hides. Diego's theorem (1966) states that finitely generated Hilbert algebras are finite: in n propositional variables there are only finitely many intuitionistically inequivalent implicational formulas, which yields decidability directly. Statman (1979) showed that the intuitionistic implicational fragment is already PSPACE-complete, whereas classical implicational validity is coNP-complete. Under Curry–Howard the intuitionistic theorems are exactly the types inhabited by closed simply typed λ-terms — K and S are the types of λx.λy.x and λx.λy.λz.xz(yz) — and normalization of terms is cut elimination on the proof side; both hold. The bases BCK, BCI and BCIW pick out the affine, linear and relevant subfragments, so the substructural hierarchy is fixed by the choice of combinators before any sequent calculus is written.

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: ⊥, ¬, ∧ and ∨ are not definable from → alone, so it is a fragment and not a logic anyone reasons in, and adding ⊥ repairs this only classically — intuitionistically ∧ and ∨ remain primitive. The fragment's apparent tractability is deceptive: intuitionistic implicational validity is PSPACE-complete and classical implicational validity coNP-complete, so the smallest interesting fragment is already as hard as the full propositional logic in each case. The single-axiom literature is a sport: those axioms prove nothing the three-axiom presentation does not. Its Curry–Howard image is the simply typed λ-calculus, which admits no fixed-point combinator, so recursion is unavailable and the fragment supports no theory of computation without added constants such as System T's recursor.

© 2026 Lingenic LLC