Models of an extension of the theory ${\bf ORD}$.
Nicholas J. De Lillo · Notre Dame Journal of Formal Logic · 1979
In [1], the first-order theory ORD was introduced as a concrete example of a theory in which the proof-theoretic concepts of implicit and explicit definability can be illustrated.Here, we use the concept of implicit definability as a means of constructing a conservative extension of certain first-order theories.The construction is then applied to ORD to yield a conservative extension ORD*.It is then shown that, under certain closure conditions on the domain A of any of the underlying models of ORD*, A is (up to isomorphism) an ordinal.Thus, in this sense, ORD* is a formal characterization of ordinal numbers in first-order logic.1 The axioms of ORD and ORD* As was described in [1], ORD is a first-order theory with equality, with the four binary relation symbols «, c ? c, and e representing the only extra-logical symbols in its alphabet.The axiom set Γ o for ORD consists of the universal closures of the following ten wffs: (O,) [(*CJOΛ(J;CS)]-(*CS)