Carlson proposes to work on a far reaching program centering on the proof theory of systems of set theory which includes a semantic approach to proof theory in general and a new method for constructing ordinal notation systems for theories of sets. The set theories to be studied initially go up to and include Zermelo-Frankel set theory with the power set axiom removed but there is some likelihood that the methods will extend much farther. The notation systems lay bare a fundamental part of the structures for the corresponding set theories. The proposed research is motivated by questions which arise naturally from Godel's incompleteness theorems. These theorems imply that no reasonable mathematical system is strong enough to provide solutions to all concrete mathematical problems, e.g., determining the existence of solutions in the natural numbers to polynomial equations or verifying the correctness of computer programs. There will always be questions whose solution will hinge on the discovery of new axioms- new axioms whose acceptance will be determined by intuition. The possible new axioms which have emerged all fall into the class of "axioms of infinity" which assert the existence of larger and larger nonconcrete mathematical objects. That axioms of this sort are the only new axioms amenable to our intuition seems possible, even probable. The ultimate goal of the proposed research would be to provide convincing answers to the following questions: 1. Can the notion of axiom of infinity be given a precise definition? 2. Can all meaningful concrete mathematical problems be resolved by axioms of infinity? 3. Which axioms of infinity are necessary for the solution of meaningful concrete mathematical questions? While answers to these questions seem unlikely in the near future, especially for the first two, the successful completion of the program proposed here would be a significant step forward.
