{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,3]],"date-time":"2025-12-03T17:28:57Z","timestamp":1764782937700},"reference-count":26,"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":8777,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1990,3]]},"abstract":"<jats:p>The <jats:italic>condensed detachment rule<\/jats:italic>, or <jats:italic>rule<\/jats:italic><jats:bold>D<\/jats:bold>, was first proposed by Carew Meredith in the 1950's for propositional logic based on implication. It is a combination of modus ponens with a \u201cminimal\u201d amount of substitution. We shall give a precise detailed statement of rule <jats:bold>D<\/jats:bold>. (Some attempts in the published literature to do this have been inaccurate.)<\/jats:p><jats:p>The <jats:bold>D<\/jats:bold>-<jats:italic>completeness question<\/jats:italic> for a given set of logical axioms is whether every formula deducible from the axioms by modus ponens and substitution can be deduced instead by rule <jats:bold>D<\/jats:bold> alone. Under the well-known formulae-as-types correspondence between propositional logic and combinator-based type-theory, rule <jats:bold>D<\/jats:bold> turns out to correspond exactly to an algorithm for computing principal type-schemes in combinatory logic. Using this fact, we shall show that <jats:bold>D<\/jats:bold> is complete for intuitionistic and classical implicational logic. We shall also show that <jats:bold>D<\/jats:bold> is incomplete for two weaker systems, BCK- and BCI-logic.<\/jats:p><jats:p>In describing the formulae-as-types correspondence it is common to say that combinators correspond to proofs in implicational logic. But if \u201cproofs\u201d means \u201cproofs by the usual rules of modus ponens and substitution\u201d, then this is not true. It only becomes true when we say \u201cproofs by rule <jats:bold>D<\/jats:bold>\u201d; we shall describe the precise correspondence in Corollary 6.7.1 below.<\/jats:p><jats:p>This paper is written for readers in propositional logic and in combinatory logic. Since workers in one field may not feel totally happy in the other, we include short introductions to both fields.<\/jats:p><jats:p>We wish to record thanks to Martin Bunder, Adrian Rezus and the referee for helpful comments and advice.<\/jats:p>","DOI":"10.2307\/2274956","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T18:33:48Z","timestamp":1146940428000},"page":"90-105","source":"Crossref","is-referenced-by-count":21,"title":["Principal type-schemes and condensed detachment"],"prefix":"10.1017","volume":"55","author":[{"given":"J. Roger","family":"Hindley","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Meredith","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200026451_ref010","first-page":"29","article-title":"The principal type-scheme of an object in combinatory logic","volume":"146","author":"Hindley","year":"1969","journal-title":"Transactions of the American Mathematical Society"},{"key":"S0022481200026451_ref014","first-page":"42","article-title":"Condensed detachment as a rule of inference","volume":"42","author":"Kalman","year":"1983","journal-title":"Stadia Logica"},{"key":"S0022481200026451_ref023","volume-title":"Formal logic","author":"Prior","year":"1955"},{"key":"S0022481200026451_ref008","volume-title":"Combinatory logic","volume":"II","author":"Curry","year":"1972"},{"key":"S0022481200026451_ref007","volume-title":"Combinatory logic","volume":"1","author":"Curry","year":"1958"},{"key":"S0022481200026451_ref004","first-page":"49","volume":"7","author":"Curry","year":"1942","journal-title":"The combinatory foundations of mathematical logic"},{"key":"S0022481200026451_ref015","first-page":"215","volume-title":"Philosophical logic","author":"Lemmon","year":"1957"},{"key":"S0022481200026451_ref025","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"S0022481200026451_ref003","first-page":"22","volume-title":"Kontrolliertes Denken. Untersuchungen zum Logikkalk\u00fcl und zur Logik der Einzelwissen-schaften (Festgabe zum 60. Geburtstag von Prof. W. Britzelmayr)","author":"Church","year":"1951"},{"key":"S0022481200026451_ref006","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1969.tb01183.x"},{"key":"S0022481200026451_ref009","unstructured":"Herbrand J. [1930], Recherches sur la th\u00e9orie de la d\u00e9monstration, thesis, University of Paris, Paris; English translation in his Logical writings (W. Goldfarb, editor), Harvard University Press, Cambridge, Massachusetts, 1971, pp. 44\u2013202."},{"key":"S0022481200026451_ref022","unstructured":"Morris J. H. [1968], Lambda-calculus models of programming languages, Ph.D. thesis, Massachusetts Institute of Technology, Cambridge, Massachusetts."},{"key":"S0022481200026451_ref026","doi-asserted-by":"publisher","DOI":"10.1007\/BF01448013"},{"key":"S0022481200026451_ref001","volume-title":"Entailment","volume":"1","author":"Anderson","year":"1975"},{"key":"S0022481200026451_ref012","volume-title":"Introduction to combinators and \u03bb-calculus","author":"Hindley","year":"1986"},{"key":"S0022481200026451_ref013","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19630091206"},{"key":"S0022481200026451_ref005","doi-asserted-by":"publisher","DOI":"10.3406\/phlou.1952.4394"},{"key":"S0022481200026451_ref020","article-title":"Condensed detachment and combinators","author":"Meyer","year":"1990","journal-title":"Journal of Automated Reasoning"},{"key":"S0022481200026451_ref011","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90100-X"},{"key":"S0022481200026451_ref016","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093957574"},{"key":"S0022481200026451_ref017","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19640101305"},{"key":"S0022481200026451_ref021","article-title":"Condensed detachment is complete for relevant logic: proof using computer","author":"Mints","year":"1990","journal-title":"Journal of Automated Reasoning"},{"key":"S0022481200026451_ref002","first-page":"33","article-title":"A result for combinators, BCK logics and BCK algebras","volume":"28","author":"Bunder","year":"1986","journal-title":"Logique et Analyse"},{"key":"S0022481200026451_ref024","volume-title":"On a theorem of Tarski","author":"Rezus","year":"1982"},{"key":"S0022481200026451_ref018","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093888116"},{"key":"S0022481200026451_ref019","doi-asserted-by":"publisher","DOI":"10.1007\/BF02124728"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200026451","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,18]],"date-time":"2019-05-18T17:51:27Z","timestamp":1558201887000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200026451\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990,3]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1990,3]]}},"alternative-id":["S0022481200026451"],"URL":"https:\/\/doi.org\/10.2307\/2274956","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1990,3]]}}}