nullane de tantis gregibus tibi digna videtur? rara avis in terra nigroque simillima cygno. Juvenal Sat. VI 161, 165. 1966-JNC visits AN at CornelI. An idea emerges. 1968-JNC is at V. c. L. A. for the Logic Year. The Los Angeles ma- script appears. 1970-AN visits JNC at Monash. 1971-The Australian manuscript appears. 1972-JNC visits AN at Cornell. Here is the result. We gratefully acknowledge support from Cornell Vniversity, Vni- versity of California at Los Angeles, Monash Vniversity and National Science Foundation Grants GP 14363, 22719 and 28169. We are deeply indebted to the many people who have helped uso Amongst the mathe- maticians, we are particularly grateful to J. C. E. Dekker, John Myhill, Erik Ellentuck, Peter AczeI, Chris Ash, Charlotte ehell, Ed Eisenberg, Dave Gillam, Bill Gross, Alan Hamilton, Louise Hay, Georg Kreisel, Phil Lavori, Ray Liggett, Al Manaster, Michael D. Morley, Joe Rosen- stein, Graham Sainsbury, Bob Soare and Michael Venning. Last, but by no means least, we thank Anne-Marie Vandenberg, Esther Monroe, Arletta Havlik, Dolores Pendell, and Cathy Stevens and the girls of the Mathematics Department of VCLA in 1968 for hours and hours of excellent typing. Thanksgiving November 1972 J. N. Crossley Ithaca, New Y ork Anil Nerode Contents O. Introduction ...1 Part 1. Categories and Functors 3 1. Categories ...3 2. Morphism Combinatorial Functors 3 3. Combinatorial Functors ...18 Part H. Model Theory . . 18 4. Countable Atomic Models 18 5. Copying . 22 6. Dimension ...26 Part III.

This book was originally intended to be the second edition of the book "Beweis theorie" (Grundlehren der mathematischen Wissenschaften, Band 103, Springer 1960), but in fact has been completely rewritten. As well as classical predicate logic we also treat intuitionistic predicate logic. The sentential calculus properties of classical formal and semiformal systems are treated using positive and negative parts of formulas as in the book "Beweistheorie." In a similar way we use right and left parts of formulas for intuitionistic predicate logic. We introduce the theory of functionals of finite types in order to present the Gi: idel interpretation of pure number theory. Instead of ramified type theory, type-free logic and the associated formalization of parts of analysis which we treated in the book "Beweistheorie," we have developed simple classical type theory and predicative analysis in a systematic way. Finally we have given consistency proofs for systems of lI -analysis following the work of G. Takeuti. In order to do this we have introduced a constni'ctive system of notation for ordinals which goes far beyond the notation system in "Beweistheorie.""