Elimination of Skolem functions for monotone formulas in analysis (Q1267846)

This is the second of a series of papers whose over-all purpose is to give estimations to the complexities of (formal) proofs of analysis. In this paper, the author develops a technical device -- elimination of Skolem functions -- to be used in subsequent work. Actually, he deals with the Herbrand normal form \(B^H\) of \(B\), and shows, roughly, that when \(B\) is monotone and \(B^H\) is provable from AC-qf in \(G_nA^\omega\), then \(B\) is provable without AC-qf and also one can extract a tuple \(\psi\) that satisfies the functional interpretation of \(B\). (For an explanation of \(G_nA^\omega\) etc., refer to the first paper [\textit{U. Kohlenbach}, ibid. 36, No. 1, 31-71 (1996; Zbl 0882.03050)].) There are many other results, including \(G_2A^\omega\lvdash \Pi^0_1\text{-AC}\to \Pi^0_1\)-[collection principle], and the like.