{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T12:54:41Z","timestamp":1682081681191},"reference-count":4,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":14894,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1973,6]]},"abstract":"<jats:p>In [4], I introduced a quasi-Boolean algebra, and showed that in a formal system of simple type theory, from which the cut rule is omitted, wffs form a quasi-Boolean algebra, and that the cut-elimination theorem can be formulated in algebraic language. In this paper we use the result of [4] to prove the cut-elimination theorem in simple type theory. The theorem was proved by M. Takahashi [2] in 1967 by using the concept of Sch\u00fctte's semivaluation. We use maximal ideals of a quasi-Boolean algebra instead of semivaluations.<\/jats:p><jats:p>The logical system we are concerned with is a modification of Sch\u00fctte's formal system of simple type theory in [1] into Gentzen style.<\/jats:p><jats:p><jats:italic>Inductive definition of types<\/jats:italic>.<\/jats:p><jats:p>0 and 1 are types.<\/jats:p><jats:p>If <jats:italic>\u03c4<\/jats:italic><jats:sub>1<\/jats:sub>, \u2026, <jats:italic>\u03c4<jats:sub>n<\/jats:sub><\/jats:italic> are types, then (<jats:italic>\u03c4<\/jats:italic><jats:sub>1<\/jats:sub>, \u2026, <jats:italic>\u03c4<jats:sub>n<\/jats:sub><\/jats:italic>) is a type.<\/jats:p><jats:p><jats:italic>Basic symbols<\/jats:italic>.<\/jats:p><jats:p><jats:italic>a<\/jats:italic><jats:sub arrange=\"stack\">1<\/jats:sub><jats:sup arrange=\"stack\">\u03c4<\/jats:sup>, <jats:italic>a<\/jats:italic><jats:sub arrange=\"stack\">2<\/jats:sub><jats:sup arrange=\"stack\">\u03c4<\/jats:sup>, \u2026 for free variables of type <jats:italic>\u03c4<\/jats:italic>.<\/jats:p><jats:p><jats:italic>x<\/jats:italic><jats:sub arrange=\"stack\">1<\/jats:sub><jats:sup arrange=\"stack\">\u03c4<\/jats:sup>, <jats:italic>x<\/jats:italic><jats:sub arrange=\"stack\">2<\/jats:sub><jats:sup arrange=\"stack\">\u03c4<\/jats:sup>, \u2026 for bound variables of type <jats:italic>\u03c4<\/jats:italic>.<\/jats:p><jats:p>An arbitrary number of constants of certain types.<\/jats:p><jats:p>An arbitrary number of function symbols with certain argument places.<\/jats:p>","DOI":"10.2307\/2272058","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T17:22:43Z","timestamp":1146936163000},"page":"215-226","source":"Crossref","is-referenced-by-count":1,"title":["A proof of the cut-elimination theorem in simple type theory"],"prefix":"10.1017","volume":"38","author":[{"given":"Satoko","family":"Titani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200077823_ref004","doi-asserted-by":"publisher","DOI":"10.2969\/jmsj\/01710072"},{"key":"S0022481200077823_ref003","doi-asserted-by":"publisher","DOI":"10.2969\/jmsj\/00730249"},{"key":"S0022481200077823_ref002","doi-asserted-by":"publisher","DOI":"10.2969\/jmsj\/01940399"},{"key":"S0022481200077823_ref001","first-page":"305","volume":"25","author":"Sch\u00fctte","year":"1960","journal-title":"Syntactical and semantical properties of simple type theory"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200077823","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T15:54:37Z","timestamp":1559231677000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200077823\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1973,6]]},"references-count":4,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1973,6]]}},"alternative-id":["S0022481200077823"],"URL":"https:\/\/doi.org\/10.2307\/2272058","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1973,6]]}}}