An abstract form of the first epsilon theorem
JOURNAL OF LOGIC AND COMPUTATION(2020)
Abstract
We present a new method of computing Herbrand disjunctions. The up-to-date most direct approach to calculate Herbrand disjunctions is based on Hilbert's 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-Bernays-Godel set theory.
MoreTranslated text
Key words
extended first epsilon theorem,sequent calculus,Herbrand disjunctions
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined