Yu, X., Riesz representation theorem, Borel measures and subsystems of second-order arithmetic, Annals of Pure and Applied Logic 59 65-78. Formalized concept of finite Borel measures is developed in the language of second-order arithmetic. Formalization of the Riesz representation theorem is proved to be equivalent to arithmetical comprehension. Codes of Borel sets of complete separable metric spaces are defined and proved to be meaningful in the subsystem ATR0. Arithmetical transfinite recursion is enough to prove the measurability of Borel sets for (...) any finite Borel measure on a compact complete separable metric space. (shrink)

Stephen George Simpson. with definition 1.2.3 and the discussion following it. For example, taking 90(n) to be the formula n §E Y, we have an instance of comprehension, VYEIXVn(n€X<—>n¢Y), asserting that for any given set Y there exists a ...

Working within weak subsystems of second-order arithmetic Z2 we consider two versions of the Baire Category theorem which are not equivalent over the base system RCA0. We show that one version (B.C.T.I) is provable in RCA0 while the second version (B.C.T.II) requires a stronger system. We introduce two new subsystems of Z2, which we call RCA+ 0 and WKL+ 0, and show that RCA+ 0 suffices to prove B.C.T.II. Some model theory of WKL+ 0 and its importance in view of (...) Hilbert's program is discussed, as well as applications of our results to functional analysis. (shrink)

Concepts of L1 space, integrable functions and integrals are formalized in weak subsystems of second order arithmetic. They are discussed especially in relation with the combinatorial principle WWKL (weak-weak König's lemma and arithmetical comprehension. Lebesgue dominated convergence theorem is proved to be equivalent to arithmetical comprehension. A weak version of Lebesgue monotone convergence theorem is proved to be equivalent to weak-weak König's lemma.

We develop measure theory in the context of subsystems of second order arithmetic with restricted induction. We introduce a combinatorial principleWWKL (weak-weak König's lemma) and prove that it is strictly weaker thanWKL (weak König's lemma). We show thatWWKL is equivalent to a formal version of the statement that Lebesgue measure is countably additive on open sets. We also show thatWWKL is equivalent to a formal version of the statement that any Borel measure on a compact metric space is countably additive (...) on open sets. (shrink)

Arithmetical comprehension is proved to be equivalent to the enumerability of singular points of any measure on the Cantor space. It is provable in ACA0 that any perfect closed subset of [0, 1] is the support of some continuous positive linear functional on C[0, 1].

We establish by elementary proof-theoretic means the conservativeness of two subsystems of analysis over primitive recursive arithmetic. The one subsystem was introduced by Friedman [6], the other is a strengthened version of a theory of Minc [14]; each has been shown to be of considerable interest for both mathematical practice and metamathematical investigations. The foundational significance of such conservation results is clear: they provide a direct finitist justification of the part of mathematical practice formalizable in these subsystems. The results are (...) generalized to relate a hierarchy of subsystems, all contained in the theory of arithmetic properties, to a corresponding hierarchy of fragments of arithmetic. The proof theoretic tools employed there are used to re-establish in a uniform, elementary way relationships between various fragments of arithmetic due to Parsons, Paris and Kirby, and Friedman. (shrink)