Classical Combinatory Logic

TL;DR

This paper introduces a new combinatory logic system that corresponds to propositional classical logic, extending the foundational understanding of logic systems and their applications in programming languages.

Contribution

It presents a combinatory logic system equivalent to the $11111111111111111111111111 system, aligning combinatory logic with classical propositional logic.

Findings

Establishes equivalence with $111111111111111111111111111 system of Barbanera and Berardi.

Provides a bridge between combinatory logic and classical propositional logic.

Abstract

Combinatory logic shows that bound variables can be eliminated without loss of expressiveness. It has applications both in the foundations of mathematics and in the implementation of functional programming languages. The original combinatory calculus corresponds to minimal implicative logic written in a system "`a la Hilbert". We present in this paper a combinatory logic which corresponds to propositional classical logic. This system is equivalent to the system $\lambda^{Sym}_{Prop}$ of Barbanera and Berardi.