ELIMINATION OF SKOLEM FUNCTIONS FOR MONOTONE FORMULAS IN ANALYSIS

In this paper a new method, elimination of Skolem functions for monoto ne formulas, is developed which makes it possible to determine precise ly the arithmetical strength of instances of various non-constructive function existence principles. This is achieved by reducing the use of such instances in a given proof to instances of certain arithmetical principles. Our framework are systems T-w := G(n)A(w) + AC-qf + Delta, where (G(n)A(w))(n epsilon N) is a hierarchy of (weak) subsystems of arithmetic in all finite types (introduced in [14]), AC-qf is the sche ma of quantifier-free choice in all types and Delta is a set of certai n analytical principles which e.g. includes the binary Konig's lemma. We apply this method to show that the arithmetical closures of single instances of Pi(1)(0)-comprehension and -choice contribute to the grow th of extractable bounds from proofs relative to T-w only by a primiti ve recursive functional in the sense of Kleene. In subsequent papers t hese results are widely generalized and the method is used to determin e the arithmetical content of single sequences of instances of the Bol zano-Weierstra ss principle for bounded sequences in R-d, the Ascoli-l emma and others.