On the Herbrand Functional Interpretation

TL;DR

This paper introduces a simplified formulation of the Herbrand functional interpretation that avoids complex set-based types, strengthening its properties and proving equivalence to the original approach.

Contribution

It presents an alternative, equivalent formulation of the Herbrand functional interpretation that simplifies types and enhances its monotonicity properties.

Findings

Simplified the types in the Herbrand interpretation

Proved equivalence between original and alternative formulations

Strengthened the monotonicity property

Abstract

We show that the types of the witnesses in the Herbrand functional interpretation can be simplified, avoiding the use of "sets of functionals" in the interpretation of implication and universal quantification. This is done by presenting an alternative formulation of the Herbrand functional interpretation, which we show to be equivalent to the original presentation. As a result of this investigation we also strengthen the monotonicity property of the original presentation, and prove a monotonicity property for our alternative definition.