{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,8,7]],"date-time":"2023-08-07T10:34:29Z","timestamp":1691404469372},"reference-count":9,"publisher":"Oxford University Press (OUP)","issue":"8","license":[{"start":{"date-parts":[[2020,9,25]],"date-time":"2020-09-25T00:00:00Z","timestamp":1600992000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,12,10]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>We present a new method of computing Herbrand disjunctions. The up-to-date most direct approach to calculate Herbrand disjunctions is based on Hilbert\u2019s epsilon formalism (which is in fact also the oldest framework for proof theory). The algorithm to calculate Herbrand disjunctions is an integral part of the proof of the extended first epsilon theorem. This paper introduces a more abstract form of epsilon proofs, the function variable proofs. This leads to a computational improved version of the extended first epsilon theorem, which allows a nonelementary speed up of the computation of Herbrand disjunctions. As an application, sequent calculus proofs are translated into function variable proofs and a variant of the axiom of global choice is shown to be removable from proofs in Neumann\u2013Bernays\u2013G\u00f6del set theory.<\/jats:p>","DOI":"10.1093\/logcom\/exaa044","type":"journal-article","created":{"date-parts":[[2020,9,2]],"date-time":"2020-09-02T11:27:38Z","timestamp":1599046058000},"page":"1447-1468","source":"Crossref","is-referenced-by-count":1,"title":["An abstract form of the first epsilon theorem"],"prefix":"10.1093","volume":"30","author":[{"given":"Matthias","family":"Baaz","sequence":"first","affiliation":[{"name":"Institute of Discrete Mathematics and Geometry 104, TU Wien, 1040 Vienna, Austria"}]},{"given":"Alexander","family":"Leitsch","sequence":"additional","affiliation":[{"name":"Institute of Logic and Computation (E192), TU Wien, 1040 Vienna, Austria"}]},{"given":"Anela","family":"Lolic","sequence":"additional","affiliation":[{"name":"Institute of Discrete Mathematics and Geometry 104, TU Wien, 1040 Vienna, Austria"}]}],"member":"286","published-online":{"date-parts":[[2020,9,25]]},"reference":[{"key":"2020120307171882600_ref1","doi-asserted-by":"crossref","first-page":"669","DOI":"10.2178\/jsl\/1333566645","article-title":"On the complexity of proof deskolemization","volume":"77","author":"Baaz","year":"2012","journal-title":"Journal of Symbolic Logic"},{"key":"2020120307171882600_ref2","doi-asserted-by":"crossref","first-page":"353","DOI":"10.3233\/FI-1994-2044","article-title":"On skolemization and proof complexity","volume":"20","author":"Baaz","year":"1994","journal-title":"Fundamenta Informaticae"},{"key":"2020120307171882600_ref3","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/S0168-0072(98)00026-8","article-title":"Cut normal forms and proof complexity","volume":"97","author":"Baaz","year":"1999","journal-title":"Annals of Pure and Applied Logic"},{"key":"2020120307171882600_ref4","volume-title":"Methods of Cut-Elimination","author":"Baaz","year":"2011"},{"key":"2020120307171882600_ref5","volume-title":"The Consistency of the Axiom of Choice and the Generalized Continuum Hypothesis with the Axioms of Set Theory","author":"G\u00f6del","year":"1940"},{"key":"2020120307171882600_ref6","volume-title":"Grundlagen der Mathematik","author":"Hilbert","year":"1939"},{"key":"2020120307171882600_ref7","doi-asserted-by":"crossref","first-page":"234","DOI":"10.2307\/2275028","article-title":"Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken","author":"Luckhardt","year":"1989","journal-title":"Journal of Symbolic Logic"},{"key":"2020120307171882600_ref8","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/BF00370646","article-title":"A compact representation of proofs","volume":"46","author":"Miller","year":"1987","journal-title":"Studia Logica"},{"key":"2020120307171882600_ref9","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/s11225-006-6610-7","article-title":"The epsilon calculus and Herbrand complexity","volume":"82","author":"Moser","year":"2006","journal-title":"Studia Logica"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/8\/1447\/34673226\/exaa044.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/8\/1447\/34673226\/exaa044.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,3]],"date-time":"2020-12-03T12:20:07Z","timestamp":1606998007000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/30\/8\/1447\/5911457"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,25]]},"references-count":9,"journal-issue":{"issue":"8","published-online":{"date-parts":[[2020,9,25]]},"published-print":{"date-parts":[[2020,12,10]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exaa044","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2020,12]]},"published":{"date-parts":[[2020,9,25]]}}}