Logic of Combinatory Logic

TL;DR

This paper introduces a classical propositional logic framework for reasoning about combinatory logic, including syntax, axioms, and semantics, and proves soundness and completeness of the system.

Contribution

It develops a formal propositional logic for combinatory logic with soundness and completeness proofs, bridging logic and combinatory reasoning.

Findings

Soundness and completeness of the axiomatic system

Semantics based on applicative structures with primitive combinators

Equational theory aligns with the propositional logic framework

Abstract

We develop a classical propositional logic for reasoning about combinatory logic. We define its syntax, axiomatic system and semantics. The syntax and axiomatic system are presented based on classical propositional logic, with typed combinatory terms as basic propositions, along with the semantics based on applicative structures extended with special elements corresponding to primitive combinators. Both the equational theory of untyped combinatory logic and the proposed axiomatic system are proved to be sound and complete w.r.t. the given semantics. In addition, we prove that combinatory logic is sound and complete w.r.t. the given semantics.