BCK Logic

Origin. Meredith (1960s), named for B, C, K combinators. Implication without contraction or weakening. Between minimal and intuitionistic. 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: Modified form holds. Γ, A ⊢ B implies Γ ⊢ A → B But restrictions on hypothesis use.

BCK algebras: Residuated poset with: x · (x → y) ≤ y x ≤ y → (x · y) Additional BCK conditions.

Extensions: BCIW = intuitionistic logic BCK + contraction = intuitionistic BCW = affine logic

Symbols.

Metatheory. Decidable. BCK algebras complete. Combinator correspondence. Cut elimination.

Applies to. Substructural hierarchy. Combinator logic. Weak implication. Resource-insensitive reasoning.

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

© 2026 Lingenic LLC