{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:09:00Z","timestamp":1763467740195},"reference-count":9,"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":11699,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1982,3]]},"abstract":"<jats:p>In [4] Gordon Plotkin considers the problem of characterizing the <jats:italic>\u03bb<\/jats:italic>-definable functionals in full type structures. A plausible, but, as we shall see, quite false, conjecture is that a functional is <jats:italic>\u03bb<\/jats:italic>-definable \u21d4 it is invariant in the sense of Fraenkel and Mostowski. A better guess might be that the set of <jats:italic>\u03bb<\/jats:italic>-definable functionals of type <jats:italic>\u03c3<\/jats:italic> has a uniform (in <jats:italic>\u03c3<\/jats:italic>) definition in type theory over all full type structures (Plotkin explicitly considers a certain sort of definition by means of \u201clogical relations\u201d). More or less generally, one may ask if the following question is decidable.<\/jats:p><jats:p>Given: a functional <jats:italic>F<\/jats:italic> in a full type structure over a finite ground domain.<\/jats:p><jats:p>Question: is <jats:italic>F<\/jats:italic><jats:italic>\u03bb<\/jats:italic>-definable?<\/jats:p><jats:p>We call the statement that this question is decidable Plotkin's <jats:italic>\u03bb<\/jats:italic>-definability conjecture. We do not know if Plotkin's conjecture is true.<\/jats:p><jats:p>In this note we consider several questions which quickly arise from Plotkin's conjecture. In <jats:italic>\u00a7<\/jats:italic>1, we ask which type structures satisfy <jats:italic>\u03bb<\/jats:italic>-definability = invariance. We construct for each consistent set of equations a model satisfying this equality. From consideration of these models we obtain a number of syntactic corollaries including a reduction of <jats:italic>\u03b2\u03b7<\/jats:italic>-conversion to <jats:italic>\u03b2\u03b7<\/jats:italic>-conversion at a single type (Theorem 3), an \u201c<jats:italic>\u03c9<\/jats:italic>-rule\u201d for <jats:italic>\u03b2\u03b7<\/jats:italic>-conversion (Proposition 6) and consistency with <jats:italic>\u03b2\u03b7<\/jats:italic>-conversion (Proposition 8), definability and indefinability results for versions of Kronecker's <jats:italic>\u03b4<\/jats:italic> (Propositions 10 and 11), and a decidability result for the problem of inter-definability among combinators.<\/jats:p>","DOI":"10.2307\/2273377","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T21:58:32Z","timestamp":1146952712000},"page":"17-26","source":"Crossref","is-referenced-by-count":65,"title":["Completeness, invariance and <i>\u03bb<\/i>-definability"],"prefix":"10.1017","volume":"47","author":[{"given":"R.","family":"Statman","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200044662_ref007","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(76)90021-9"},{"key":"S0022481200044662_ref004","volume-title":"\u03bb-definability and logical relations","author":"Plotkin","year":"1973"},{"key":"S0022481200044662_ref008","volume-title":"Natural deduction","author":"Prawitz","year":"1965"},{"key":"S0022481200044662_ref009","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71129-7"},{"key":"S0022481200044662_ref005","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(79)90007-0"},{"key":"S0022481200044662_ref006","first-page":"123","volume-title":"Lecture Notes in Mathematics","volume":"344","author":"Troelstra","year":"1973"},{"key":"S0022481200044662_ref003","first-page":"213","volume-title":"Lecture Notes in Computer Science","volume":"37","author":"Jacopini","year":"1975"},{"key":"S0022481200044662_ref001","volume-title":"Combinatory logic","volume":"1","author":"Curry","year":"1968"},{"key":"S0022481200044662_ref002","first-page":"22","volume-title":"Lecture Notes in Mathematics","volume":"453","author":"Friedman","year":"1975"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200044662","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,24]],"date-time":"2019-05-24T21:42:22Z","timestamp":1558734142000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200044662\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1982,3]]},"references-count":9,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1982,3]]}},"alternative-id":["S0022481200044662"],"URL":"https:\/\/doi.org\/10.2307\/2273377","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1982,3]]}}}