On the equivalence of systems of rules and systems of axioms in illative combinatory logic.
Martin W. Bunder · Notre Dame Journal of Formal Logic · 1979
The most useful systems of illative combinatory logic contain the primitive Ξ for restricted generality with the rule:or alternatively the primitive F or the primitives P and Π with their appropriate rules. 1 ' 2 In addition they have for (combinatory) equality:Rule Eq // X = Y, then X h Y, and a deduction rule for Ξ (or for F or for P and Π) such as for example that of [1]:where Δ is any sequence of terms and V is not free in Δ, X or Y, then Δ, FAHX^ZXY. 3 Often however, such systems are set up using in addition to Rule Ξ and Rule Eq, a set of axioms, and the deduction rule is derived as a theorem.