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

108 Views Asked by At

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?

1

There are 1 best solutions below

0
On

There is no constructive proof of the compactness of the interval of (Cauchy or Dedekind) real numbers [0, 1]. In particular it is not compact for computable real numbers. This is because there are bounded computable sequences of computable real numbers which do not converge to a computable real number.

You are using decidability whenever you say something of the form either p or not p. It's good that you've made it explicit. The law of excluded middle is used to show this for all propositions. There is no reason to expect that membership in this way is decidable (and it in general is not). So yes, you are using LEM here since that fact is neither always true nor self-evident.