Classical Type Theory with Transfinite Types

摘要

This paper defines a system of classical logic that includes transfinite typesformed by means of the general Cartesian product operation. The consistency of the system is established by means of a semantical argument.... Mathematical logic, Deduction and theorem proving.