{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T06:20:32Z","timestamp":1761805232105},"reference-count":31,"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":7497,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1993,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators or, in a more direct way, in which derivations are not translated. Both translations are closely related in a canonical way. The two direct translations turn out to be complete. The paper fulfills the program of Church [1932], [1933] and Curry [1930] to base logic on a consistent system of \u03bb-terms or combinators. Hitherto this program had failed because systems of ICL were either too weak (to provide a sound interpretation) or too strong (sometimes even inconsistent).<\/jats:p>","DOI":"10.2307\/2275096","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T18:49:16Z","timestamp":1146941356000},"page":"769-788","source":"Crossref","is-referenced-by-count":9,"title":["Systems of illative combinatory logic complete for first-order propositional and predicate calculus"],"prefix":"10.1017","volume":"58","author":[{"given":"Henk","family":"Barendregt","sequence":"first","affiliation":[]},{"given":"Martin","family":"Bunder","sequence":"additional","affiliation":[]},{"given":"Wil","family":"Dekkers","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200020880_ref017","doi-asserted-by":"publisher","DOI":"10.2307\/1968167"},{"key":"S0022481200020880_ref004","unstructured":"Barendsen E. [1989], Representation of logic, data types and recursive functions in typed lambda calculi, Masters Thesis, Department of Computer Science, Catholic University, Nijmegen."},{"key":"S0022481200020880_ref028","doi-asserted-by":"publisher","DOI":"10.2307\/1968646"},{"key":"S0022481200020880_ref022","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.28.12.564"},{"key":"S0022481200020880_ref011","first-page":"771","volume":"48","author":"Bunder","year":"1983","journal-title":"A weak absolute consistency proof for some systems of illative combinatory logic"},{"key":"S0022481200020880_ref001","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71252-7"},{"key":"S0022481200020880_ref015","doi-asserted-by":"publisher","DOI":"10.2307\/1968422"},{"key":"S0022481200020880_ref027","volume-title":"Introduction to combinators and \u03bb-calculus","author":"Hindley","year":"1986"},{"key":"S0022481200020880_ref007","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093891196"},{"key":"S0022481200020880_ref009","doi-asserted-by":"publisher","DOI":"10.1007\/BF02023007"},{"key":"S0022481200020880_ref013","volume-title":"The calculi of lambda conversion","author":"Church","year":"1941"},{"key":"S0022481200020880_ref018","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.20.11.584"},{"key":"S0022481200020880_ref016","doi-asserted-by":"publisher","DOI":"10.2307\/2370900"},{"key":"S0022481200020880_ref012","doi-asserted-by":"publisher","DOI":"10.2307\/1968337"},{"key":"S0022481200020880_ref025","volume-title":"Combinatory logic, Vol. 1","author":"Curry","year":"1958"},{"key":"S0022481200020880_ref021","first-page":"371","article-title":"First properties of functionality in combinatory logic","volume":"41","author":"Curry","year":"1936","journal-title":"T\u00f4hoku Mathematical Journal"},{"key":"S0022481200020880_ref023","first-page":"49","volume":"7","author":"Curry","year":"1942","journal-title":"The combinatory foundations of mathematical logic"},{"key":"S0022481200020880_ref019","doi-asserted-by":"publisher","DOI":"10.2307\/1968498"},{"key":"S0022481200020880_ref002","volume-title":"The lambda calculus, its syntax and semantics","author":"Barendregt","year":"1984"},{"key":"S0022481200020880_ref005","unstructured":"Bunder M. W. [1969], Set theory based on combinatory logic, Ph.D. thesis, Department of Mathematics, University of Amsterdam."},{"key":"S0022481200020880_ref026","volume-title":"Combinatory logic, Vol. 2","author":"Curry","year":"1972"},{"key":"S0022481200020880_ref010","doi-asserted-by":"publisher","DOI":"10.1007\/BF02023016"},{"key":"S0022481200020880_ref030","first-page":"107","volume":"16","author":"Mostowski","year":"1951","journal-title":"On the rules of proof in the pure functional calculus of first order"},{"key":"S0022481200020880_ref024","first-page":"115","volume":"7","author":"Curry","year":"1942","journal-title":"The inconsistency of certain formal logics"},{"key":"S0022481200020880_ref031","volume-title":"Een opmerking over intuitionistische logica","author":"Peremans","year":"1949"},{"key":"S0022481200020880_ref014","doi-asserted-by":"publisher","DOI":"10.2307\/2370716"},{"key":"S0022481200020880_ref029","first-page":"115","volume":"20","author":"L\u00f6b","year":"1955","journal-title":"A solution of a problem of Henkin"},{"key":"S0022481200020880_ref020","first-page":"654","article-title":"Foundations of the theory of abstract sets from the standpoint of combinatory logic","volume":"40","author":"Curry","year":"1935","journal-title":"Bulletin of the American Mathematical Society"},{"key":"S0022481200020880_ref006","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093890997"},{"key":"S0022481200020880_ref008","first-page":"467","volume":"41","author":"Bunder","year":"1976","journal-title":"The inconsistency of"},{"key":"S0022481200020880_ref003","volume-title":"Handbook of logic in computer science, Vol. II","author":"Barendregt","year":"1992"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200020880","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T18:02:54Z","timestamp":1557943374000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200020880\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,9]]},"references-count":31,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1993,9]]}},"alternative-id":["S0022481200020880"],"URL":"https:\/\/doi.org\/10.2307\/2275096","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,9]]}}}