arXiv · 2111.12133
On extracting variable Herbrand disjunctions
Abstract
Some quantitative results obtained by proof mining take the form of Herbrand disjunctions that may depend on additional parameters. We attempt to elucidate this fact through an extension to first-order arithmetic of the proof of Herbrand's theorem due to Gerhardy and Kohlenbach which uses the functional interpretation.
Explore related subjects
Keep this discovery
Andrei Sipos. 2021-11-23. On extracting variable Herbrand disjunctions. https://arxiv.org/abs/2111.12133
Cite the original work for its findings. Save a collection to share your selection of sources.