On extracting variable Herbrand disjunctions

DOI10.1007/S11225-022-09990-5MaRDI QIDQ6383790arXivWikidataFDO

Authors Andrei Sipoş

Publication date 23 November 2021

Published in arXiv

Full work available at URL https://doi.org/10.1007/S11225-022-09990-5

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Functionals in proof theory (03F10) First-order arithmetic and fragments (03F30)

arXiv classification

math.LO

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.

This page was built for publication: On extracting variable Herbrand disjunctions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6383790)