Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus (Q1267843)

The idea of illative combinatory logic ILC -- which has its roots in the pioneering work of Curry and Church in the early thirties -- is to extend usual combinatory logic, which is an equational theory of (self-applicable) operations, with a kind of abstract deducibility relation, in order to represent ordinary logic and even mathematics in ILC. The program of ILC is challenging and not easy to implement: since the early work of the founding fathers Curry and Church, many systems have been proposed and some of them were found inconsistent or too weak, others still need a consistency proof. The present paper is the continuation of the 1993 paper of the authors [\textit{H. Barendregt, M. Bunder} and \textit{W. Dekkers}, ``Systems of illative combinatory logic complete for first-order propositional and predicate calculus'', J. Symb. Logic 58, 769-788 (1993; Zbl 0791.03006)], where they investigate systems of ILC which are well-suited for representing propositional and elementary predicate calculus. The main result concerns completeness theorems for two indirect translations of two systems of ILC (by ``indirect translation'' the authors mean an interpretation which does not exploit the propositions-as-types idea). Roughly, the typical theorem states that if the translation of \(A\) is derivable in a system of ILC from the translation of a set \(X\) of premises, then \(A\) is derivable from \(X\) in predicate (or propositional) logic. It is important to stress that these results imply the consistency of the ILC-systems; they also round off the soundness and completeness theorems for direct and indirect translations. The paper is not self-contained and it can be read only with an adequate acquaintance with the cited 1993 paper. The methods of proofs are syntactical (for instance, cut elimination is applied).