On extracting variable Herbrand disjunctions

TL;DR

This paper extends Herbrand's theorem proof in first-order arithmetic using functional interpretation to clarify how Herbrand disjunctions depend on parameters in proof mining.

Contribution

It introduces an extension to first-order arithmetic that elucidates the parametric dependence of Herbrand disjunctions in proof mining.

Findings

Provides a new proof extension for Herbrand's theorem

Clarifies the parametric dependence in Herbrand disjunctions

Enhances understanding of proof mining techniques

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.