Wolfram Library Archive

Courseware Demos MathSource Technical Notes
All Collections Articles Books Conference Proceedings

Reasoning About Iteration in Gödel's Class Theory

Johan Gijsbertus Frederik Belinfante
Organization: Georgia Institute of Technology
Journal / Anthology

Automated Deduction - Cade-19
Year: 2003
Volume: LNCS 2741
Page range: 228-242

A computer implementation of Gödel's algorithm for class for- mation in Mathematica 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.

*Mathematics > Foundations of Mathematics > Logic
*Mathematics > Foundations of Mathematics > Set Theory
Related items

*Gödel's Algorithm for Class Formation   [in Articles]