{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,11,15]],"date-time":"2023-11-15T00:21:13Z","timestamp":1700007673433},"reference-count":20,"publisher":"Wiley","issue":"6","license":[{"start":{"date-parts":[[2008,11,4]],"date-time":"2008-11-04T00:00:00Z","timestamp":1225756800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Mathematical Logic Qtrly"],"published-print":{"date-parts":[[2008,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper we show some non\u2010elementary speed\u2010ups in logic calculi: Both a predicative second\u2010order logic and a logic for fixed points of positive formulas are shown to have non\u2010elementary speed\u2010ups over first\u2010order logic. Also it is shown that eliminating second\u2010order cut formulas in second\u2010order logic has to increase sizes of proofs super\u2010exponentially, and the same in eliminating second\u2010order epsilon axioms. These are proved by relying on results due to P. Pudl\u00e1k. (\u00a9 2008 WILEY\u2010VCH Verlag GmbH &amp; Co. KGaA, Weinheim)<\/jats:p>","DOI":"10.1002\/malq.200710067","type":"journal-article","created":{"date-parts":[[2008,11,4]],"date-time":"2008-11-04T13:53:03Z","timestamp":1225806783000},"page":"629-640","source":"Crossref","is-referenced-by-count":2,"title":["Non\u2010elementary speed\u2010ups in logic calculi"],"prefix":"10.1002","volume":"54","author":[{"given":"Toshiyasu","family":"Arai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2008,11,4]]},"reference":[{"key":"e_1_2_1_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/772062.772068"},{"key":"e_1_2_1_3_2","first-page":"667","article-title":"On interpretability in theories containing arithmetic II","volume":"22","author":"H\u00e1jek P.","year":"1981","journal-title":"Comm. Math. Univ. Carol."},{"key":"e_1_2_1_4_2","doi-asserted-by":"crossref","unstructured":"P.H\u00e1jek andP.Pudl\u00e1k Metamathematics of First\u2010Order Arithmetic (Springer 1993).","DOI":"10.1007\/978-3-662-22156-3"},{"key":"e_1_2_1_5_2","unstructured":"D.Hilbert andP.Bernays Grundlagen der Mathematik vol. II (Springer 1939)."},{"key":"e_1_2_1_6_2","doi-asserted-by":"publisher","DOI":"10.2307\/2275451"},{"key":"e_1_2_1_7_2","unstructured":"A. C.Leisenring Mathematical Logic and Hilbert's\u03b5\u2010Symbol (Gordon and Breach 1969)."},{"key":"e_1_2_1_8_2","doi-asserted-by":"publisher","DOI":"10.2969\/jmsj\/00740323"},{"key":"e_1_2_1_9_2","first-page":"419","article-title":"Equality axioms on Hilbert's \u03b5 \u2010symbol","volume":"7","author":"Maehara S.","year":"1957","journal-title":"J. Faculty of Science, University of Tokyo, Section I"},{"key":"e_1_2_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-006-6610-7"},{"key":"e_1_2_1_11_2","doi-asserted-by":"publisher","DOI":"10.2969\/jmsj\/02440684"},{"key":"e_1_2_1_12_2","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19820283306"},{"key":"e_1_2_1_13_2","doi-asserted-by":"crossref","unstructured":"N.Motohashi \u03b5\u2010theorems and elimination theorems of uniqueness conditions. In: Patras Logic Symposion pp. 373\u2013387 (North\u2010Holland 1982).","DOI":"10.1016\/S0049-237X(08)71374-0"},{"key":"e_1_2_1_14_2","first-page":"137","article-title":"Lower bounds for the lengthening of proofs after cut\u2010elimination (in Russian)","volume":"88","author":"Orevkov V. P.","year":"1982","journal-title":"Zapiski Nauchnykh Seminarov LOMI"},{"key":"e_1_2_1_15_2","doi-asserted-by":"crossref","unstructured":"P.Pudl\u00e1k On the length of proofs of finitistic consistency statements in first\u2010order theories. In: Logic Colloquium 84 (J. B. Paris A. J. Wilkie and G. M. Wilmers eds.) pp. 165\u2013196 (North\u2010Holland 1986).","DOI":"10.1016\/S0049-237X(08)70462-2"},{"key":"e_1_2_1_16_2","doi-asserted-by":"crossref","unstructured":"P.Pudl\u00e1k The lengths of proofs. In: Handbook of Proof Theory (S. R. Buss ed.) pp. 547\u2013637 (North\u2010Holland 1998).","DOI":"10.1016\/S0049-237X(98)80023-2"},{"key":"e_1_2_1_17_2","unstructured":"J.Shoenfield Mathematical Logic (Addison\u2010Wesley 1967). Reprinted from ASL 2001."},{"key":"e_1_2_1_18_2","doi-asserted-by":"crossref","unstructured":"S. G.Simpson Subsystems of Second Order Arithmetic (Springer 1999).","DOI":"10.1007\/978-3-642-59971-2"},{"key":"e_1_2_1_19_2","doi-asserted-by":"publisher","DOI":"10.2307\/2042682"},{"key":"e_1_2_1_20_2","unstructured":"G.Takeuti Proof Theory second edition (North\u2010Holland 1987)."},{"key":"e_1_2_1_21_2","doi-asserted-by":"crossref","unstructured":"A. S.Troelstra andH.Schwichtenberg Basic Proof Theory second edition. Cambridge Tracts in Theoretical Computer Science 43 (Cambridge University Press 2000).","DOI":"10.1017\/CBO9781139168717"}],"container-title":["Mathematical Logic Quarterly"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fmalq.200710067","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fmalq.200710067","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/malq.200710067","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,14]],"date-time":"2023-11-14T13:48:09Z","timestamp":1699969689000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/malq.200710067"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,11,4]]},"references-count":20,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2008,12]]}},"alternative-id":["10.1002\/malq.200710067"],"URL":"https:\/\/doi.org\/10.1002\/malq.200710067","archive":["Portico"],"relation":{},"ISSN":["0942-5616","1521-3870"],"issn-type":[{"value":"0942-5616","type":"print"},{"value":"1521-3870","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,11,4]]}}}