A formal characterization of ordinal numbers.
Nicholas J. De Lillo · Notre Dame Journal of Formal Logic · 1973
In this paper we present the axioms for a first-order finitely axiomatized theory ORD, some of whose models are relational systems S with the following particular characteristics:(i) S, the domain of discourse of £, is any ordinal number; and(ii) each primitive relation symbol of the alphabet of ORD is interpreted in S in the standard manner.Of special importance is the fact, demonstrated below, that ORD is an example of a theory in which the proof-theoretic notions of explicit and implicit definability, as stated in Beth [l], [2] and Smullyan [3], may be illustrated.1 Basic Concepts.Let T be a first-order theory whose non-logical axioms are the set of sentences denoted by Γ o .Let P, P l9 P 2 . . .be the relation symbols of the alphabet of T which occur in at least one member of Γ o .In addition, P will be assumed to be an rc-place relation symbol for some positive integer n.P is explicitly definable from P l9 P 2 . . . in T if there exists a wff U(x ί9 x 29 . ..,# w ), all of whose relation symbols occur in the list P ί9 P 2 . .., such thatLet P f be a relation symbol of the alphabet of T having the same number of places as P. Assume P f does not occur in Γ o , and let Γ£ be the result of substituting P' for P in every sentence of Γ o in which P appears.P is implicitly definable from P l9 P•,*«) ^ ^'(*i,*2, .,*«)].2 The Theory ORD.The first-order theory ORD is, basically, a theory with equality, such that the four binary relation symbols, ~, c, c, and e