Model-theoretic studies on subsystems of second order arithmetic
Takeshi Yamazaki · Tohoku Mathematical Publications · 2000
This research is motivated by the following theme originated with H. Friedman: very often, if a theorem τ of ordinary mathematics is proved from the "right" set existence axioms, τ is equivalent to those axioms over some weaker system in which τ itself is not provable.This theme is referred to as Reverse mathematics.Here, we focus on three subsystems RCA 0 , WKL 0 and ACA 0 of second order arithmetic and a second order system BTFA of 0-1 strings.By RCA 0 , we mean the system of recursive comprehension axioms with Σ 0 1 induction.WKL 0 consists of RCA 0 plus weak König's lemma which asserts that every infinite 0-1 tree has a path.The first-order part of WKL 0 is the same as that of RCA 0 .ACA 0 consists of RCA 0 plus arithmetical comprehension axioms.The first order part of ACA 0 is just first order Peano arithmetic PA.The acronym BTFA stands for base theory for feasible analysis.BTFA is conservative over Polynomial Time Computable Arithmetic PTCA with respect to the Π 0 2 sentences.In chapter 2, we study models of RCA 0 +Π 0 ∞ -BCT and WKL 0 .Π 0 ∞ -BCT is a version of the Baire category theorem introduced by Brown and Simpson.We show the following