BCK Logic

Origin. Meredith (1960s), named for B, C, K combinators. Implication with weakening but without contraction — K is weakening, so it is contraction alone that is dropped. This is the affine implicational fragment, strictly weaker than the intuitionistic one. Combinator correspondence. Foundation for weak implications.

Models. BCK algebras. Residuated structures without contraction. Term models from combinators. Kripke models with restricted accessibility.

Formalism.

Combinator basis: B: (A → B) → (C → A) → C → B (composition) C: (A → B → C) → B → A → C (flip) K: A → B → A (constant)

Axiom system: A → A (identity) (A → B) → ((C → A) → (C → B)) (B) (A → B → C) → (B → A → C) (C) A → B → A (K)

Missing from intuitionistic: No W: (A → A → B) → A → B (contraction) Cannot duplicate hypotheses.

Deduction theorem: Γ, A ⊢ B implies Γ ⊢ A → B, provided the derivation uses A at most once. Without W the hypothesis cannot be duplicated, so the unrestricted form fails.

BCK algebras: Residuated poset with: x · (x → y) ≤ y y ≤ x → (x · y) The two are the counit and unit of the residuation adjunction x · y ≤ z iff y ≤ x → z. Additional BCK conditions: integrality (the monoid unit is the top), which is what corresponds to weakening.

Extensions: BCK itself = the affine implicational fragment (weakening, no contraction) BCI = the linear fragment (drop K: neither weakening nor contraction) BCIW = R→, the relevant implicational fragment (contraction, no weakening) — not intuitionistic BCKW = BCK + contraction = the positive implicational calculus, the intuitionistic fragment

Symbols.

Metatheory. BCK is the implicational fragment of the affine logic FLew: exchange and weakening are available and contraction is not, which is why K is an axiom and W is not. Its sequent calculus admits cut elimination, and because no rule duplicates a formula, proof search terminates and the logic is decidable; Meyer and Ono, "The finite model property for BCK and BCIW" (1994), established the finite model property. BCK is algebraizable and complete with respect to the class of BCK-algebras, which Wroński, "BCK-algebras do not form a variety" (1983), showed is a quasivariety only: it is closed under subalgebras and products but not under homomorphic images. Bounded commutative BCK-algebras are term-equivalent to MV-algebras, so Łukasiewicz infinite-valued logic is an axiomatic extension of BCK. Under Curry–Howard the theorems of BCK are exactly the types inhabited by affine λ-terms. BCK is a proper sublogic of the positive implicational calculus, which it becomes on adding W.

Applies to. Substructural hierarchy. Combinator logic. Weak implication. Affine resource reasoning: a resource may be discarded but not duplicated.

Limitations. The deduction theorem holds only in restricted form — Γ, A ⊢ B yields Γ ⊢ A → B when the derivation uses A at most once — because without W a hypothesis cannot be discharged twice. Consequently S, (A → (B → C)) → ((A → B) → (A → C)), is not a theorem, nor is the contraction axiom (A → (A → B)) → (A → B), so BCK proves strictly less than the intuitionistic implicational calculus and cannot reconstruct it. Weakening makes it irrelevant: A → (B → A) is an axiom, premises need not be used, and the variable-sharing property fails, so BCK is not a relevance logic. Being purely implicational it defines no negation, conjunction, or disjunction. And since BCK-algebras form a quasivariety and not a variety, they are not axiomatizable by identities and Birkhoff's HSP theorem does not apply to them.

© 2026 Lingenic LLC