论 Herbrand 函数解释

我们证明了 Herbrand 函数解释中见证者的类型可以被简化，从而避免在对蕴涵和全称量化进行解释时使用“泛函集合”。这是通过给出 Herbrand 函数解释的一种替代表述来实现的，我们证明其与原始表述等价。作为该研究的成果，我们还加强了原始表述的单调性性质，并证明了我们替代定义的单调性性质。