On extracting variable Herbrand disjunctions
Logic
2022-02-25 v2
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.
Cite
@article{arxiv.2111.12133,
title = {On extracting variable Herbrand disjunctions},
author = {Andrei Sipos},
journal= {arXiv preprint arXiv:2111.12133},
year = {2022}
}