Number-theoretic set theories.
Paul S. Strauss · Notre Dame Journal of Formal Logic · 1985
In Section 1 we shall describe a system, WTN, which is a natural extension of pure number theory, and where all individual variables range over the natural numbers.This system avoids Gόdel constructions of undecidable sentences.In Section 2 we prove some elementary theorems in WTN.In Section 3 we consider ordinal numbers, and also indicate a proof of the axiom of choice.In Section 4 we consider cardinal numbers, in particular we show that all sets are countable in WTN.In Section 5 we consider real numbers.Here we discuss the problem of doing Lebesgue measure theory in WTN.In Section 5 we also consider a theorem related to Herbrand's Theorem.In Section 6 we consider related systems (this section can be read right after Section 2).The system WTN was first announced in [7], and has certain similarities with [2], [12], and [13]. / The system WTNLet PN be classical pure number theory, i.e., Peano arithmetic.For definiteness, we consider it formalized as in [4], p. 82, but for simplicity we consider ~ for negation, D for implication, and (z) for universal quantification as the only primitive logical connectives (cf.[4], p. 406, Ex. 2).Furthermore, we identify the symbols of the system and strings of symbols with their Gόdel numbers according to a customary assignment.We use the logical notation of [5], in particular the dot notation.And we shall use Xx, ΛΓ 2 , ... as the individual variables.We sometimes use x, y for x x , x 2i respectively.We use z, w, w, υ, p, q, r, s, t, c, d, with or without subscripts, as meta-variables ranging over the individual variables of our system.We use α and b as terms.We identify natural numbers with nonnegative integers, although it is of some interest to consider them identified with positive integers instead, particularly in our treatment of real numbers (cf.Section 5), but we shall not do so here.There is a primitive recursive function v such that if m is a natural number then v(m) is the numeral of m (hence v(m) is also a natural number).We sometimes write 0, 1,..., m for v(0), v(l), ..., v(m), respectively.