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) → ((B → C) → (A → C)) (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. Decidable. BCK algebras complete. Combinator correspondence. Cut elimination.

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

Limitations. Very weak. No contraction. Limited expressiveness. Theoretical interest mainly.

© 2026 Lingenic LLC