  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.
