{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T06:45:45Z","timestamp":1648709145495},"reference-count":4,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":12885,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1978,12]]},"abstract":"<jats:p>In [1, \u00a714E], a sequent calculus formulation (<jats:italic>L<\/jats:italic>.-formulation) of type assignment (theory of functionality) is given for a system based either on a system of combinators with strong reduction or on a system of \u03bb\u03b7-calculus provided that the rule for subject conversion (which says that if <jats:italic>X<\/jats:italic> has type \u03b1 and <jats:italic>X<\/jats:italic> cnv <jats:italic>Y<\/jats:italic> then <jats:italic>Y<\/jats:italic> has type \u03b1) is postulated for the system. This sequent calculus formulation does not work for a system based on the \u03bb\u03b2-calculus. In [2] I introduced a sequent calculus formulation for a system without the rule of subject conversion based on any of the three systems mentioned above. Further, in [2, \u00a75] I pointed out that if proper inclusions of the form of the statement that \u03bb<jats:italic>x<\/jats:italic>\u00b7<jats:italic>x<\/jats:italic> is a function from \u03b1 to \u03b2 are postulated, then functions are identified with their restrictions in the \u03bb\u03b7-calculus but not in the \u03bb\u03b2-calculus, and that therefore there is some interest in having a sequent calculus formulation of type assignment with the rule of subject conversion for systems based on the \u03bb\u03b2-calculus. In this paper, such a system is presented, the elimination theorem (Gentzen's <jats:italic>Hauptsatz<\/jats:italic>) is proved for it, and it is proved equivalent to the natural deduction formulation of [1, \u00a714D].<\/jats:p><jats:p>I shall assume familiarity with the \u03bb\u03b2-calculus, and shall use (with minor modifications) the notational conventions of [1]. Hence, the theory of type assignment (theory of functionality) will be based on an atomic constant F such that if \u03b1 and \u03b2 are types then F\u03b1\u03b2 represents roughly the type of functions from \u03b1 to \u03b2 (more exactly it represents the type of functions whose domain includes \u03b1 and under which the image of \u03b1 is included in \u03b2).<\/jats:p>","DOI":"10.2307\/2273503","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T21:48:57Z","timestamp":1146952137000},"page":"643-649","source":"Crossref","is-referenced-by-count":1,"title":["A sequent calculus formulation of type assignment with equality rules for the \u03bb\u03b2-calculus"],"prefix":"10.1017","volume":"43","author":[{"given":"Jonathan P.","family":"Seldin","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S002248120004915X_ref001","volume-title":"Combinatory logic","volume":"II","author":"Curry","year":"1972"},{"key":"S002248120004915X_ref003","unstructured":"Seldin J. P. , Studies in illative combinatory logic, Dissertation, University of Amsterdam, 1968."},{"key":"S002248120004915X_ref004","unstructured":"Seldin J. P. , The theory of generalized functionality. I, unpublished manuscript."},{"key":"S002248120004915X_ref002","first-page":"11","volume":"42","author":"Seldin","year":"1977","journal-title":"A sequent calculus for type assignment"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S002248120004915X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T19:07:58Z","timestamp":1558984078000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S002248120004915X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1978,12]]},"references-count":4,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1978,12]]}},"alternative-id":["S002248120004915X"],"URL":"https:\/\/doi.org\/10.2307\/2273503","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1978,12]]}}}