Elimination of Skolem functions for monotone formulas in analysis |
| |
Authors: | Ulrich Kohlenbach |
| |
Institution: | Fachbereich Mathematik, J.W. Goethe-Universit?t, D-60054 Frankfurt, Germany, DE
|
| |
Abstract: | In this paper a new method, elimination of Skolem functions for monotone formulas, is developed which makes it possible to
determine precisely 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 -qf , where (GA is a hierarchy of (weak) subsystems of arithmetic in all finite types (introduced in 14]), AC-qf is the schema of quantifier-free
choice in all types and is a set of certain analytical principles which e.g. includes the binary K?nig's lemma. We apply this method to show that
the arithmetical closures of single instances of -comprehension and -choice contribute to the growth of extractable bounds from proofs relative to only by a primitive recursive functional in the sense of Kleene. In subsequent papers these results are widely generalized
and the method is used to determine the arithmetical content of single sequences of instances of the Bolzano-Weierstra? principle
for bounded sequences in , the Ascoli-lemma and others.
February 14, 1996 |
| |
Keywords: | Mathematics Subject Classification: 03F35 03F10 03F03 03F25 |
本文献已被 SpringerLink 等数据库收录! |
|