# Attempt at constructive proof of compactness of [0,1], does this use LEM? Does a constructive proof exist?

Suppose I start a proof off with "Let $U_x$ be an open cover of $[0,1]$. Either $[0,1] \in U_x$ or $[0,1] \notin U_x$." Am I using the Law of the Excluded Middle here, or is this fact somehow evident without that assumption?

Also, does a constructive proof (interpreted loosely) of the compactness of $[0,1]$ exist? Is the standard proof constructive in any sense? Asked another way, is there an algorithm (again, interpreted loosely) that takes an open cover of $[0,1]$ and returns a finite open cover?

• Yes, you are using the Law. What exactly do you mean by "a constructive proof" and why do you think that the Law of the Excluded Middle makes a proof non-constructive? I mean, what's non-constructive about checking whether an element is in a set and deciding upon that? Feb 20, 2018 at 16:30
• @freakish Because Andrej Bauer said so. But seriously, I guess my reason is because it doesn't hold in every topos. But on the other hand, your question makes me realize I don't understand why LEM can't be used in proves that are constructive in the sense that they provide an algorithm for obtaining the existence of any object promised by the proof. So feel free to interpret "constructive" somewhat loosely in your answer, even if it involves explaining how the standard proof is in some sense "constructive." Feb 20, 2018 at 16:38
• @freakish I missed your edit when I was typing my response. We are thinking along the same lines. I know I've heard that constructivists can use LEM when they've demonstrated that the property they are talking about is of the kind that is susceptible to LEM (not that I really know what that means). Feb 20, 2018 at 16:40
• I have some intuition but this is beyond my level of formal understanding unfortunately. I'm very interested in an answer though. Feb 20, 2018 at 16:42
• This PDF suggests to me that LEM is very important for compactness. You might find it illuminating. Feb 20, 2018 at 16:53