Artificial Intelligence as a Possible Tool for Discovering Laws of Logic

The present essay has its origins in some technical work I did several years ago in mathematical logic. At that time I was busy in an obscure area on the borders of set theory and proof theory trying to describe notations for transfinite ordinals. (The best known example of this sort of result is Cantor's description of a "normal form" for certain countable ordinals. One builds notations for these ordinals out of some basic functions and the resulting description is similar to the ordinary Indian notation for finite numbers.) As time passed, I found myself increasingly puzzled by the circumstance that although I could manipulate my ideas with some facility, I really had no clear notion of what I was doing. From one point of view, my unease was not justified: if one made use of a few notions from standard set theory--some material about ordinal functions, "inaccessible ordinals" of various sorts, e tc . -one could obtain a neat, classical description of the situation (Buchholz, 1975). But this "description" seemed to miss the mark for it did not provide an elucidation of what I felt was the basically computational and procedural nature of the experience that I underwent. I felt, in some vague way, that I was just doing a construction and that an adequate explication should be a description of the essentials of this construction. The set-theoretic "explanation" lacked any dynamic quality. Confused by this circumstance, I began to pay more attention to the introductory chapters of the various texts on logic and mathematical logic that I was using in my teaching, for it was there that was usually concentrated a discussion of what was called "foundations of mathematics," a discussion which, I naively thought, justified the long and intricate technical chapters which followed. In fact, most of these chapters (if