{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,12]],"date-time":"2024-01-12T13:02:05Z","timestamp":1705064525553},"reference-count":7,"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":17816,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1965,6]]},"abstract":"<jats:p>This paper deals with Hilbert's substitution method for eliminating bound variables from first order proofs. With a first order system <jats:italic>S<\/jats:italic> framed in the \u03b5-calculus [2] the problem is to associate a system <jats:italic>S<\/jats:italic>' without bound variables and an effective procedure for transforming derivations in <jats:italic>S<\/jats:italic> into derivations in <jats:italic>S<\/jats:italic>\u2032. The transform of a formula <jats:italic>A<\/jats:italic> derived in <jats:italic>S<\/jats:italic> is to be an \u201c\u03b5-substitution instance\u201d of <jats:italic>A<\/jats:italic>, i.e. it is obtained by replacing terms <jats:sub>\u03b5x<\/jats:sub><jats:italic>B(x)<\/jats:italic> in <jats:italic>A<\/jats:italic> by terms of <jats:italic>S<\/jats:italic>\u2032. In general the choice of these terms will depend on the particular derivation of <jats:italic>A<\/jats:italic>, and not on <jats:italic>A<\/jats:italic> alone. Cf. [4]. The present formulation sharpens Hilbert's original statement of the problem, i.e. that the transform of <jats:italic>A<\/jats:italic> should be finitistically verifiable, by making explicit the methods of verification used, namely those formalized in <jats:italic>S<\/jats:italic>\u2032; on the other hand, it generalizes Hilbert's formulation since <jats:italic>S<\/jats:italic>\u2032 need not be restricted to finitist systems.<\/jats:p><jats:p>The bound variable elimination procedure can always be taken to be primitive recursive in (the G\u00f6del number of) the derivation of <jats:italic>A<\/jats:italic>. Constructions which transcend primitive recursion can simply be built into <jats:italic>S<\/jats:italic>\u2032.<\/jats:p><jats:p>In this paper we show that if <jats:italic>S<\/jats:italic>\u2032 is taken to be a second order system with constants for functionals, then the existence of suitable \u03b5-substitution instances can be expressed by the solvability of certain functional equations in <jats:italic>S<\/jats:italic>\u2032. We deal with two cases here. If <jats:italic>S<\/jats:italic> is number theory without induction, i.e. essentially predicate calculus with identity, then we can solve the equations in question by taking for <jats:italic>S<\/jats:italic>\u2032 the free variable part <jats:italic>S<\/jats:italic>* of <jats:italic>S<\/jats:italic> with an added rule of definition of functionals by cases (recursive definition on finite ordinals), which is a conservative extension of <jats:italic>S<\/jats:italic>*.<\/jats:p>","DOI":"10.2307\/2270133","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T20:28:25Z","timestamp":1146947305000},"page":"175-192","source":"Crossref","is-referenced-by-count":19,"title":["The substitution method"],"prefix":"10.1017","volume":"30","author":[{"given":"W. W.","family":"Tait","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200056619_ref005","first-page":"155","volume":"30","author":"Tait","year":"1965","journal-title":"Functionals defined by transfinite recursion"},{"key":"S0022481200056619_ref001","doi-asserted-by":"publisher","DOI":"10.1007\/BF01450016"},{"key":"S0022481200056619_ref002","volume-title":"Grundlagen der Mathematik, II","author":"Hilbert","year":"1939"},{"key":"S0022481200056619_ref003","first-page":"241","volume":"16","author":"Kreisel","year":"1951","journal-title":"On the interpretation of non-finitist proofs, Part I"},{"key":"S0022481200056619_ref004","doi-asserted-by":"publisher","DOI":"10.1007\/BF01192912"},{"key":"S0022481200056619_ref006","unstructured":"Tait W. W. , The no-counterexample interpretation for arithmetic. To appear."},{"key":"S0022481200056619_ref007","unstructured":"Tait W. W. , The no-counterexample interpretation for ramified analysis. To appear."}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200056619","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,3]],"date-time":"2019-06-03T19:41:26Z","timestamp":1559590886000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200056619\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1965,6]]},"references-count":7,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1965,6]]}},"alternative-id":["S0022481200056619"],"URL":"https:\/\/doi.org\/10.2307\/2270133","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1965,6]]}}}