Higher-order illative combinatory logic (Q2869904)

Systems of illative combinatory logic or lambda calculus were introduced by Schönfinkel, Curry and Church as foundations of logic and mathematics. These systems, however were proved inconsistent by Kleene and Rosser.NEWLINENEWLINEA restriction to the introduction rule for restricted generality \(\Xi\), in [\textit{M. W. Bunder}, Notre Dame J. Formal Logic 15, 25--34 (1974; Zbl 0212.02504)] led to a weak consistency proof (not all terms are provable) of quite general systems [\textit{M. W. Bunder}, J. Symb. Log. 48, 771--776 (1983; Zbl 0527.03003)]. At last, in [\textit{H. Barendregt} et al., J. Symb. Log. 58, No. 3, 769--788 (1993; Zbl 0791.03006); \textit{W. Dekkers} et al., J. Symb. Log. 63, No. 3, 869--890 (1998; Zbl 0947.03018); \textit{W. Dekkers} et al., Arch. Math. Logic 37, No. 5--6, 327--341 (1998; Zbl 0908.03016)] were strong systems of illative combinatory logic proved consistent in the strong sense that not all propositions are provable. Unfortunately, these proofs do not cover a simple axiom needed for the definitions of some of the standard connectives and quantifiers.NEWLINENEWLINEThe current very important paper gives a strong consistency proof for a system that does include this axiom but has a weaker version of one important rule. While this system allows the development of (even classical) predicate logic of arbitrarily high order, the proof given doesn't guarantee its consistency. While the Barendregt, Bunder, Dekkers proofs are syntactic, the author's proof is a model theoretic one and relies on the existence of a model of higher-order predicate calculus. However, as shown in [\textit{M. W. Bunder}, Stud. Log. 47, No. 2, 129--143 (1988; Zbl 0664.03015)], the class of natural numbers can be defined in such a way that all except one of the Peano axioms of arithmetic are derivable in the system the author proves strongly consistent. So, the author provides a strong consistency proof for much of arithmetic! Of course, if the missing axiom (\(x''=Y''\to X=Y\)) were included his result might contradict Gödel's theorem.