On Computer-Assisted Proofs in Ordinal Number Theory |
| |
| Authors: | Johan G F Belinfante |
| |
| Affiliation: | (1) School of Mathematics, Georgia Institute of Technology, USA |
| |
| Abstract: | Some basic theorems about ordinal numbers were proved using McCune s computer program OTTER, building on Quaifes modification of Gödels class theory. Our theorems are based on Isbells elegant definition of ordinals. Neither the axiom of regularity nor the axiom of choice is used. |
| |
| Keywords: | OTTER ordinal numbers set theory |
| 本文献已被 SpringerLink 等数据库收录！ |
