2
$\begingroup$

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?

$\endgroup$
8
  • $\begingroup$ 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? $\endgroup$
    – freakish
    Feb 20, 2018 at 16:30
  • $\begingroup$ @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." $\endgroup$
    – user52969
    Feb 20, 2018 at 16:38
  • $\begingroup$ @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). $\endgroup$
    – user52969
    Feb 20, 2018 at 16:40
  • $\begingroup$ I have some intuition but this is beyond my level of formal understanding unfortunately. I'm very interested in an answer though. $\endgroup$
    – freakish
    Feb 20, 2018 at 16:42
  • 1
    $\begingroup$ This PDF suggests to me that LEM is very important for compactness. You might find it illuminating. $\endgroup$ Feb 20, 2018 at 16:53

1 Answer 1

2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.