Ordinal theory in a conservative extension of predicate calculus.
John H. Harris · Notre Dame Journal of Formal Logic · 1971
Let P f denote the class-set theory which consists of just axioms Al, A2, A3 and theorem M3 (restricted to case n = 1) of [2].Simplifying a little, P' is thus basically a first order theory with equality having two sorts of variables, class variables and set variables, and satisfying an axiom of extensionality and an axiom schema which says the following: for any wff which contains no bound class variables there is a class X of all sets v satisfying φ; in symbols IX \fv [υ eX+-*φ(υ)].(As usual for class and set variables we use capital and small letters respectively.)By [3] theory P f is a conservative extension of P 9 the firstorder predicate calculus with equality where the only non-logical symbol is "e" and the individual variables are the set variables.The purpose of this paper is to show that a surprisingly large portion of the theory of Von-Neumann ordinals and natural numbers can be developed in P\ Such information could be useful in the investigation of any formulation of set theory not using the unrestricted subset axiom VYVx [YQx -FeV] which involves unrestricted quantification over class variables in an essential way.An example of such a restricted set theory would be a formalization of the set theoretical reasoning used in predicative analysis; cf.[1].By [3] our results are equally valid for a corresponding conservative class extension K r of any first-order theory K.In such a case one would have in general three types of individual variables: K, set, and class variables.We say R is a (strict) linear-ordering of X (abbrev.: Lo R (X)) if and only if R is irreflexive, connected and transitive over X; in symbols lrr R (X), i.e., (Vu) x π (uRu) Con R (X), i.e., (Vu,υ) x [uRυ v u = υ v vRu] Tr R (X), i.e., (Vu,v, w)χ [uRv .vRw -+uRw]