A type-free system extending (ZFC) (Q1121865)

The authors define a further extension \((EFL)^*\) of Aczel's type-free theory of Frege structures [cf. \textit{P. Aczel}, The Kleene Symp., Proc., Madison/Wis. 1978, Stud. Logic Found. Math. 101, 31-59 (1980; Zbl 0462.03002), and \textit{R. Flagg} and \textit{J. Myhill}, Mathematical logic and theoretical computer science, Lect. Notes Pure Appl. Math. 106, 197- 217 (1987; Zbl 0662.03051)] to allow interpretation of ZFC. The language of this theory is that of type-free \(\lambda\)-calculus over the primitive constants \(=\), \({\mathcal N}\), \({\mathcal P}\), \(\vee\), \&, \(\Rightarrow\), \(\exists\), \(\forall\). Here, e.g., (values of) terms \({\mathcal P}A\), \(\forall (\lambda x.{\mathcal P}(Cx))\) and \({\mathcal N}M\), respectively, correspond to the assertions: ``A is a true or false proposition'', ``C is a class (or propositional function)'', and ``M is a Church's \(\lambda\)-numeral (i.e. M is \(\lambda fx.f^ m(x))\), \(m=0,1,2,...)''\). The authors postulate well-known rules for equality (i.e. for terms \(=AB)\) and also for other primitive constants. Then the Comprehension Rule, which allows to infer \(\exists f \forall x\in A \phi (x,fx)\) from ``A is a discrete class'' and \(\forall x\in A \exists !y \phi (x,y)\), gives rise to the second-order arithmetic with full comprehension. To interpret ZFC the authors add a formal closure property of the collection of discrete classes, namely, that the universe (of functions) is well ordered so that some of its initial segments is both discrete and strongly inaccessible. Given a suitable \(\kappa\)-continuous model \(D_{\kappa}=[D_{\kappa}\to D_{\kappa}]\) of \(\lambda\)-calculus with \(\kappa\) strongly inaccessible, the author inductively define (following the ideas of F. B. Fitch, D. Scott and P. Aczel [cf. \textit{P. Aczel}, loc. cit.]) the corresponding Frege structure (the primitive constants \(=\), \({\mathcal N}\),... are interpreted in \(D_{\kappa}\) as \(\lambda xy.<0,x,y>\), \(\lambda x.<1,x>\), etc., and the subsets \({\mathcal T},{\mathcal F}\subseteq D_{\kappa}\) of true and, respectively, false propositions are defined to satisfy \({\mathcal P}a\in {\mathcal F}\) iff \(a\in {\mathcal T}\cup {\mathcal F}\), \(\Rightarrow ab\in {\mathcal F}\) iff \(a\in {\mathcal T}\) and \(b\in {\mathcal F}\), etc.). This gives a consistency proof of \((EFL)^*\). Finally, in connection with a theorem of Friedman's, it is asked whether there exists a combinatory algebra in which the scheme \(\forall \bar x \forall \bar y[\&_{ij}(x_ i=x_ j\Rightarrow y_ i=y_ j)\Rightarrow \exists f \&_ i(fx_ i=y_ i)]\) is valid.