A constructive Knaster-Tarski proof of the uncountability of the reals
History and Overview
2019-02-21 v1 Logic
Abstract
We give an uncountability proof of the reals which relies on their order completeness instead of their sequential completeness. We use neither a form of the axiom of choice nor the law of excluded middle, therefore the proof applies to the MacNeille reals in any flavor of constructive mathematics. The proof leans heavily on Levy's unusual proof of the uncountability of the reals.
Keywords
Cite
@article{arxiv.1902.07366,
title = {A constructive Knaster-Tarski proof of the uncountability of the reals},
author = {Ingo Blechschmidt and Matthias Hutzler},
journal= {arXiv preprint arXiv:1902.07366},
year = {2019}
}
Comments
two pages, adapted from Eliahu Levy's proof