Resolution and the consistency of analysis

It is shown by a purely syntactic argument how the completeness of resolution in type theory implies the consistency of type theory with axioms of extensionality, descriptions, and infinity. In this system the natural numbers are defined, and Peanos Postulates proved; indeed, classical analysis and much more can be formalized here. Nevertheless, Godels results show that the completeness of resolution in type theory cannot be proved in this system. Mathematical Offprint Service classification numbers: O2B15 Higher order predicate calculus O2G99 Methodology of deductive systems 68A40 Theorem proving This research was partially supported by NSF Grant GJ-28457X. Resolution and the Consistency of Analysis Peter B. Andrews §