A constructive Knaster-Tarski proof of the uncountability of the reals

TL;DR

This paper presents a constructive proof of the uncountability of real numbers based on order completeness, avoiding classical assumptions like the axiom of choice, and extends to MacNeille reals.

Contribution

It introduces a novel constructive proof leveraging the Knaster-Tarski theorem and order completeness, applicable to various constructive real number systems.

Findings

Proof applies to MacNeille reals in constructive mathematics

Avoids use of axiom of choice and law of excluded middle

Leverages Levy's proof technique for uncountability

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.