Toward Mechanical Mathematics

Results are reported here of a rather successful attempt of proving all theorems, totalling near 400, of Principia Mathematica which are strictly in the realm of logic, viz., the restricted predicate calculus with equality. A number of other problems of the same type are discussed. It is suggested that the time is ripe for a new branch of applied logic which may be called “inferential” analysis, which treats proofs as numerical analysis does calculations. This discipline seems capable, in the not too remote future, of leading to machine proofs of difficult new theorems. An easier preparatory task is to use machines to formalize proofs of known theorems. This line of work may also lead to mechanical checks of new mathematical results comparable to the debugging of a program.