Reasoning about iteration in gödel’s class theory

Abstract

A computer implementation of Gödel’s algorithm for class formation in MathematicaTM was used to formulate definitions and theorems about iteration in Gödel’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 Schröder-Bernstein theorem.