Date: 6 Dec 88 15:01:12 EST From: Francisco Corella To: info-hol@edu.ucdavis.clover Message-Id: <120688.150113.corella@ibm.com> Subject: Formulations of H.O.L. Sender: CORELLA Status: RO This is regarding Mike Gordon's question about formulating H.O.L. without defining the quantifiers in terms of the choice operator, and whether the axiom of choice would be needed. In the original formulation of H.O.L. [3] the quantifiers are primitive constants, rather than being defined in terms of the choice operator. The same is true of my natural deduction formulation of H.O.L. in [4]. In Andrews' system Q0, all logical constants (except the choice or descritpion operators), and in particular the quantifiers, are defined from the equality constant (a remarkable achievement, originally due to Henkin). The formulation fo Q0 can be found in Andrews' first book, in his paper [1], or in his second book [2]. In [1], Andrews proves the independence of the axiom of choice and related results. So the answer is: yes, the axiom of choice will be needed. - Francisco Corella (CORELLA@IBM.COM) REFERENCES: [1] P. B. Andrews, "General Models, Descriptions and Choice in Type Theory," Journal of Symbolic Logic, vol. 37 (1972) no. 2. [2] P. B. Andrews, "An Introduction to Mathematical Logic and Type Theory," Academic Press (1986). [3] A. Church, "A Formulation of the Simple Theory of Types," Journal of Symbolic Logic, vol. 5 (1940) no. 1. [4] F. Corella, "An Approach to the Mechanization of Set Theory," IBM Technical Report RC 14062 (1988).