{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,15]],"date-time":"2026-08-15T22:38:56Z","timestamp":1786833536286,"version":"build-2736575974"},"reference-count":5,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":23568,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1949,9]]},"abstract":"<jats:p>Although several proofs have been published showing the completeness of the propositional calculus (cf. Quine (1)), for the first-order functional calculus only the original completeness proof of G\u00f6del (2) and a variant due to Hilbert and Bernays have appeared. Aside from novelty and the fact that it requires less formal development of the system from the axioms, the new method of proof which is the subject of this paper possesses two advantages. In the first place an important property of formal systems which is associated with completeness can now be generalized to systems containing a non-denumerable infinity of primitive symbols. While this is not of especial interest when formal systems are considered as <jats:italic>logics<\/jats:italic>\u2014i.e., as means for analyzing the structure of languages\u2014it leads to interesting applications in the field of abstract algebra. In the second place the proof suggests a new approach to the problem of completeness for functional calculi of higher order. Both of these matters will be taken up in future papers.<\/jats:p><jats:p>The system with which we shall deal here will contain as primitive symbols<\/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=\"S0022481200105675_eqnU1\"\/><\/jats:disp-formula><\/jats:p><jats:p>and certain sets of symbols as follows:<\/jats:p><jats:p>(i) <jats:italic>propositional symbols<\/jats:italic> (some of which may be classed as <jats:italic>variables<\/jats:italic>, others as <jats:italic>constants<\/jats:italic>), and among which the symbol \u201c<jats:italic>f<\/jats:italic>\u201d above is to be included as a constant;<\/jats:p><jats:p>(ii) for each number <jats:italic>n<\/jats:italic> = 1, 2, \u2026 a set of <jats:italic>functional symbols of degree n<\/jats:italic> (which again may be separated into <jats:italic>variables<\/jats:italic> and <jats:italic>constants<\/jats:italic>); and<\/jats:p><jats:p>(iii) <jats:italic>individual symbols<\/jats:italic> among which <jats:italic>variables<\/jats:italic> must be distinguished from <jats:italic>constants<\/jats:italic>. The set of variables must be infinite.<\/jats:p>","DOI":"10.2307\/2267044","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T19:06:41Z","timestamp":1146942401000},"page":"159-166","source":"Crossref","is-referenced-by-count":291,"title":["The completeness of the first-order functional calculus"],"prefix":"10.1017","volume":"14","author":[{"given":"Leon","family":"Henkin","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200105675_ref001","doi-asserted-by":"publisher","DOI":"10.2307\/2267505"},{"key":"S0022481200105675_ref002","doi-asserted-by":"publisher","DOI":"10.1007\/BF01696781"},{"key":"S0022481200105675_ref005","volume-title":"Skrifter utgitt av Det Norske Videnskaps-Akademi i Oslo","author":"Skolem","year":"1929"},{"key":"S0022481200105675_ref003","first-page":"261","article-title":"Der Wahrheitsbegriff in den Formalisierten Sprachen","volume":"1","author":"Tarski","year":"1936","journal-title":"Studia Philosophica"},{"key":"S0022481200105675_ref004","volume-title":"Introduction to Mathematical Logic, Part I","author":"Church","year":"1944"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200105675","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T10:29:33Z","timestamp":1559989773000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200105675\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1949,9]]},"references-count":5,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1949,9]]}},"alternative-id":["S0022481200105675"],"URL":"https:\/\/doi.org\/10.2307\/2267044","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1949,9]]}}}