Cantor theorem and friends, in logical form

https://doi.org/10.1016/j.apal.2012.10.011Get rights and content
Under an Elsevier user license
open archive

Abstract

We prove a generalization of the hyper-game theorem by using an abstract version of inductively generated formal topology. As applications we show proofs for Cantor theorem, uncountability of the set of functions from N to N and Gödel theorem which use no diagonal argument.

MSC

03B22
03F40
03F65

Keywords

Formal topology
Abstract proof system
Hyper-game
Well-founded part of a relation

Cited by (0)