Reasoning about Iteration in Godel's Class Theory

摘要

A computer implementation of Godel's algorithm for class formation in Mathematica~(TM) was used to formulate definitions and theorems about iteration in Godel's class theory. The intent is to use this approach for automated reasoning about a variety of applications of iteration using McCune's automated reasoning program otter. The applications include the theory of transitive closures of relations, the arithmetic of natural numbers, construction of invariant subsets, and the Schroder-Bernstein theorem.