Constructive Order Types |
Other editions - View all
Common terms and phrases
A₁ a₂ analogues B₁ bracket symbol C₁ Cantor Normal Form chapter classical ordinals Clearly completes the proof Cons F contradiction corollary CROSSLEY D₁ definition DEKKER and MYHILL'S denote directed refinement theorem E-numbers embedded enumeration equivalent exist finite follows at once hence by theorem Immediate from theorem implies initial segment integers isolated least upper bound leave the reader Let AEA limit number linear ordering linearly ordered sets losols minimal upper bounds natural numbers notation number for addition number for exponentiation numbers for multiplication obtain one-one partial recursive order preserving order type ordinal sum P₁ P₂ partial recursive function principal numbers proof of theorem prove Q₁ quasi-finite C.O.T.s quasi-well-ordering r.e. set recursive descending chain recursive function defined recursive isomorphism recursive set separation lemma sequence number similarly Suppose transfinite induction undefined otherwise unique write