{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T23:05:24Z","timestamp":1779145524178,"version":"3.51.4"},"reference-count":8,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":21195,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1956,3]]},"abstract":"<jats:p>In part I of this paper it is shown that if the simple theory of types (with an axiom of infinity) is consistent, then so is the system obtained by adjoining axioms of extensionality; in part II a similar metatheorem for G\u00f6del-Bernays set theory will be proved. The first of these results is of particular interest because type theory without the axioms of extensionality is fundamentally rather a simple system, and it should, I believe, be possible to prove that it is consistent.<\/jats:p><jats:p>Let us consider \u2014 in some unspecified formal system \u2014 a typical expression of the axiom of extensionality; for example:<\/jats:p><jats:p><jats:disp-formula><jats:graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" orientation=\"portrait\" mime-subtype=\"gif\" mimetype=\"image\" position=\"float\" xlink:type=\"simple\" xlink:href=\"S0022481200085352_equ1\"\/><\/jats:disp-formula><\/jats:p><jats:p>where <jats:bold>A<\/jats:bold>(<jats:italic>h<\/jats:italic>) is a formula, and <jats:bold>A<\/jats:bold>(<jats:italic>f<\/jats:italic>), <jats:bold>A<\/jats:bold>(<jats:italic>g<\/jats:italic>) are the results of substituting in it the predicate variagles <jats:italic>f, g<\/jats:italic> for the free variable <jats:italic>h.<\/jats:italic> Evidently, if the system considered contains the predicate calculus, and if <jats:italic>h<\/jats:italic> occurs in <jats:bold>A<\/jats:bold>(<jats:italic>h<\/jats:italic>) only in parts of the form <jats:italic>h<\/jats:italic>(<jats:bold>t<\/jats:bold>) where <jats:bold>t<\/jats:bold> is a term which lies within the range of the quantifier (<jats:italic>x<\/jats:italic>), then 1.1 will be provable. But this will not be so in general; indeed, by introducing into the system an intensional predicate of predicates we can make 1.1 <jats:italic>false<\/jats:italic>. For example, Myhill introduces a constant <jats:italic>S<\/jats:italic>, where \u2018<jats:italic>S\u03d5\u03c8\u03c7\u03c9<\/jats:italic>\u2019 means that (the expression) \u03d5 is the result of substituting \u03c8 for \u03c7 in \u03c9.<\/jats:p>","DOI":"10.2307\/2268484","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T19:41:18Z","timestamp":1146944478000},"page":"36-48","source":"Crossref","is-referenced-by-count":21,"title":["On the axiom of extensionality \u2013 Part I"],"prefix":"10.1017","volume":"21","author":[{"given":"R. O.","family":"Gandy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200085352_ref005","first-page":"56","volume":"5","author":"Church","year":"1940","journal-title":"A formulation of the simple theory of types"},{"key":"S0022481200085352_ref006","first-page":"1","article-title":"Probleme der Grundlegung der Mathematik","volume":"102","year":"1929","journal-title":"Mathematische Annalen"},{"key":"S0022481200085352_ref003","first-page":"69","volume":"4","author":"Robinson","year":"1939","journal-title":"On the independence of the axioms of definiieness"},{"key":"S0022481200085352_ref004","first-page":"245","volume-title":"The logical syntax of language","author":"Carnap","year":"1937"},{"key":"S0022481200085352_ref001","first-page":"35","volume":"16","author":"Myhill","year":"1951","journal-title":"The consistency of the axiom of reducibility"},{"key":"S0022481200085352_ref002","volume-title":"Translations from the philosophical writings of Gottlob Frege","year":"1952"},{"key":"S0022481200085352_ref007","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.24.12.556"},{"key":"S0022481200085352_ref008","first-page":"28","volume":"7","author":"Newman","year":"1942","journal-title":"A formal theorem in Church's theory of types"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200085352","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T05:17:14Z","timestamp":1559884634000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200085352\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1956,3]]},"references-count":8,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1956,3]]}},"alternative-id":["S0022481200085352"],"URL":"https:\/\/doi.org\/10.2307\/2268484","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1956,3]]}}}