{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T11:28:14Z","timestamp":1777894094553,"version":"3.51.4"},"reference-count":33,"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":8593,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1990,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Church's simple theory of types is a system of higher-order logic in which functions are assumed to be total. We present in this paper a version of Church's system called <jats:bold>PF<\/jats:bold> in which functions may be partial. The semantics of <jats:bold>PF<\/jats:bold>, which is based on Henkin's general-models semantics, allows terms to be nondenoting but requires formulas to always denote a standard truth value. We prove that <jats:bold>PF<\/jats:bold> is complete with respect to its semantics. The reasoning mechanism in <jats:bold>PF<\/jats:bold> for partial functions corresponds closely to mathematical practice, and the formulation of <jats:bold>PF<\/jats:bold> adheres tightly to the framework of Church's system.<\/jats:p>","DOI":"10.2307\/2274487","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T22:36:50Z","timestamp":1146955010000},"page":"1269-1291","source":"Crossref","is-referenced-by-count":67,"title":["A partial functions version of Church's simple theory of types"],"prefix":"10.1017","volume":"55","author":[{"given":"William M.","family":"Farmer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S002248120002569X_ref033","doi-asserted-by":"publisher","DOI":"10.2307\/2024549"},{"key":"S002248120002569X_ref030","first-page":"714","volume":"50","author":"Shapiro","year":"1985","journal-title":"Second-order languages and mathematical practice"},{"key":"S002248120002569X_ref029","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0061839"},{"key":"S002248120002569X_ref028","volume-title":"Logics without existence assumptions","author":"Schock","year":"1968"},{"key":"S002248120002569X_ref027","doi-asserted-by":"publisher","DOI":"10.2307\/2369948"},{"key":"S002248120002569X_ref024","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16492-8_94"},{"key":"S002248120002569X_ref021","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093957655"},{"key":"S002248120002569X_ref020","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90011-0"},{"key":"S002248120002569X_ref018","first-page":"81","volume":"15","author":"Henkin","year":"1950","journal-title":"Completeness in the theory of types"},{"key":"S002248120002569X_ref017","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4"},{"key":"S002248120002569X_ref016","first-page":"73","volume-title":"VLSI specification, verification, and synthesis","author":"Gordon","year":"1987"},{"key":"S002248120002569X_ref015","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010277"},{"key":"S002248120002569X_ref014","volume-title":"Tenth international conference on automated deduction","author":"Farmer"},{"key":"S002248120002569X_ref012","first-page":"579","volume-title":"To H. B. Curry: essays on combinatory logic, lambda calculus andformalism","author":"de Bruijn","year":"1980"},{"key":"S002248120002569X_ref008","first-page":"56","volume":"5","author":"Church","year":"1940","journal-title":"A formulation of the simple theory of types"},{"key":"S002248120002569X_ref006","first-page":"51","volume-title":"Logic, Methodology and Philosophy of Science VII","author":"Beeson","year":"1986"},{"key":"S002248120002569X_ref005","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-68952-9"},{"key":"S002248120002569X_ref003","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0012885"},{"key":"S002248120002569X_ref013","unstructured":"Feferman S. , Polymorphic typed lambda-calculi in a type-free axiomatic framework, preprint, 1988."},{"key":"S002248120002569X_ref019","doi-asserted-by":"publisher","DOI":"10.4064\/fm-52-3-323-344"},{"key":"S002248120002569X_ref001","doi-asserted-by":"publisher","DOI":"10.4064\/fm-52-3-345-350"},{"key":"S002248120002569X_ref011","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"S002248120002569X_ref031","doi-asserted-by":"publisher","DOI":"10.1093\/analys\/20.6.125"},{"key":"S002248120002569X_ref025","volume-title":"PDLM: a proof development language for mathematics","author":"Monk","year":"1986"},{"key":"S002248120002569X_ref004","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/029\/09"},{"key":"S002248120002569X_ref009","volume-title":"Implementing mathematics with the nuprl proof development system","author":"Constable","year":"1986"},{"key":"S002248120002569X_ref002","volume-title":"An introduction to mathematical logic and type theory: to truth through proof","author":"Andrews","year":"1986"},{"key":"S002248120002569X_ref023","first-page":"153","volume-title":"Methodology and Philosophy of Science VI","author":"Martin-L\u00f6f","year":"1982"},{"key":"S002248120002569X_ref022","doi-asserted-by":"publisher","DOI":"10.4064\/fm-62-2-125-164"},{"key":"S002248120002569X_ref026","doi-asserted-by":"publisher","DOI":"10.1093\/mind\/XIV.4.479"},{"key":"S002248120002569X_ref007","doi-asserted-by":"publisher","DOI":"10.2307\/2025179"},{"key":"S002248120002569X_ref032","first-page":"59","article-title":"Foundations of partial type theory","volume":"14","author":"Tich\u00fd","year":"1982","journal-title":"Reports on Mathematical Logic"},{"key":"S002248120002569X_ref010","first-page":"183","volume-title":"Symposium on Logic in Computer Science","author":"Constable","year":"1987"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S002248120002569X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,18]],"date-time":"2019-05-18T20:25:09Z","timestamp":1558211109000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S002248120002569X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990,9]]},"references-count":33,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1990,9]]}},"alternative-id":["S002248120002569X"],"URL":"https:\/\/doi.org\/10.2307\/2274487","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1990,9]]}}}