{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,8,31]],"date-time":"2023-08-31T17:07:26Z","timestamp":1693501646464},"reference-count":0,"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":14072,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1975,9]]},"abstract":"<jats:p>Although a variety of proofs are available for the Craig-Lyndon Interpolation Lemma, they all seem to make essential use of negation, with the result that they are inapplicable to deductive theories in which negation cannot be expressed. It is here shown that this use of negation can be avoided by extending the Interpolation Lemma to the pure implicational calculus PC<jats:sub>I<\/jats:sub>.<\/jats:p><jats:p>Determinate Parameter Lemma. <jats:italic>For each formula A, \u22a8P<jats:sub>A<\/jats:sub> \u2283 A for some sentence parameter P<jats:sub>A<\/jats:sub> occurring in A<\/jats:italic>.<\/jats:p><jats:p>Proof. By induction on the construction of <jats:italic>A<\/jats:italic>.<\/jats:p><jats:p>Interpolation Lemma For PC<jats:sub>I<\/jats:sub>. <jats:italic>Let \u0393 be the set of sentence parameters common to A and C.If \u22a8A \u2283 and C is not valid, then there is a formula B containing no sentence parameter not in Y such that \u22a8A \u2283 B and \u22a8B \u2283 C<\/jats:italic>.<\/jats:p><jats:p>Proof. Since \u22a8<jats:italic>P<jats:sub>A<\/jats:sub><\/jats:italic> \u2283 <jats:italic>A<\/jats:italic> by the Determinate Parameter Lemma and \u22a8<jats:italic>A<\/jats:italic> \u2283 <jats:italic>C<\/jats:italic>, \u22a8<jats:italic>P<jats:sub>A<\/jats:sub><\/jats:italic> \u2283 <jats:italic>C<\/jats:italic>. But <jats:italic>C<\/jats:italic> is by hypothesis an invalid formula, so <jats:italic>P<jats:sub>A<\/jats:sub><\/jats:italic> must occur in <jats:italic>C<\/jats:italic> as well as in <jats:italic>A<\/jats:italic>. Thus <jats:italic>P<jats:sub>A<\/jats:sub><\/jats:italic> \u0404 \u0393.<\/jats:p>","DOI":"10.2307\/2272168","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T21:36:35Z","timestamp":1146951395000},"page":"443-444","source":"Crossref","is-referenced-by-count":1,"title":["An interpolation lemma for the pure implicational calculus"],"prefix":"10.1017","volume":"40","author":[{"given":"Roy","family":"Edelstein","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200053056","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T19:21:44Z","timestamp":1559157704000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200053056\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1975,9]]},"references-count":0,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1975,9]]}},"alternative-id":["S0022481200053056"],"URL":"https:\/\/doi.org\/10.2307\/2272168","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1975,9]]}}}