The pointwise ergodic theorem in subsystems of second-order arithmetic

Publisher: Cambridge University Press

E-ISSN: 1943-5886|72|1|45-66

ISSN: 0022-4812

Source: The Journal of Symbolic Logic, Vol.72, Iss.1, 2007-03, pp. : 45-66

Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.

Previous Menu Next

Abstract

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 ACA0; moreover, the pointwise ergodic theorem is equivalent to (ACA) over the base theory RCA0.