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 ${\cal T}^{\omega} :={\rm G}_n{\rm A}^{\omega} +{\rm AC}$ -qf $+\Delta$ , where (G $_n$ A $^{\omega})_{n \in {\Bbb N}}$ 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 $\Delta$ 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 $\Pi^0_1$ -comprehension and -choice contribute to the growth of extractable bounds from proofs relative to ${\cal T}^\omega$ 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 ${\Bbb R}^d$ , the Ascoli-lemma and others. (shrink)

The pointwise ergodic theorem is nonconstructive. In this paper, we examine origins of this non-constructivity, and determine the logical strength of the theorem and of the auxiliary statements used to prove it. We discuss properties of integrable functions and of measure preserving transformations and give three proofs of the theorem, though mostly focusing on the one derived from the mean ergodic theorem. All the proofs can be carried out in ACA₀; moreover, the pointwise ergodic theorem is equivalent to (ACA) over (...) the base theory RCA₀. (shrink)

We develop fundamental aspects of the theory of metric, Hilbert, and Banach spaces in the context of subsystems of second-order arithmetic. In particular, we explore issues having to do with distances, closed subsets and subspaces, closures, bases, norms, and projections. We pay close attention to variations that arise when formalizing definitions and theorems, and study the relationships between them.

Let T be a positive L₁-L∞ contraction. We prove that the following statements are equivalent in constructive mathematics. (1) The projection in L₂ on the space of invariant functions exists: (2) The sequence (Tⁿ)n∈N Cesáro-converges in the L₂ norm: (3) The sequence (Tⁿ)n∈N Cesáro-converges almost everywhere. Thus, we find necessary and sufficient conditions for the Mean Ergodic Theorem and the Dunford-Schwartz Pointwise Ergodic Theorem. As a corollary we obtain a constructive ergodic theorem for ergodic measure-preserving transformations. This answers a question (...) posed by Bishop. (shrink)