FINITE REVERSE MATHEMATICS
Harvey M. Friedman · SSRN Electronic Journal · 2001
Abstract. We present some formal systems in the language of linearly ordered rings with finite sets whose nonlogical axioms are strictly mathematical, which correspond to polynomially bounded arithmetic. With an additional strictly mathematical axiom, the systems correspond to exponentially bounded arithmetic. 1. T0 and IS0. In this section, we introduce the system T 0, and show that it corresponds to the system IS 0 of polynomially bounded arithmetic (presented below). Let T 0 be the following system in the two sorted language with variables over integers and variables over finite sets of integers. For the integer sort, we use the language 0,1,+,-,•,<, = of linearly ordered rings. We use Œ between integers and sets. Equality is used only between integers. The official integer variables are x 0,x 1,..., and the official set variables are A 0,A 1,.... The nonlogical axioms of T 0 are as follows. 1. Linearly ordered ring axioms. 2. Finite interval. ($A)("x)(x Œ A ´ (y < x Ÿ x < z)). 3. Boolean difference. ($C)("x)(x Œ C ´ (x Œ A Ÿ ÿ(x Œ