Clarification on constructivist’s counter-example

In the last maths post, I asked whether there was a proof that f ⁡ x = x + s had a root. As pointed out, it is pretty obvious in this example. What I meant to ask was whether f given worked as a counter-example in general proofs of the IVT.

The idea is that although trichotomy is an axiom of the reals (any two numbers are equal, or one larger than the other), what is actually used in proofs is something very different philosophically. It is distinct to say no more that some one of the three cases holds; or that a particular one of the three cases holds. The function given shows exactly the divide. While s is clearly a real by construction, and thus trichotomy with any other real holds. Because however we cannot determine whether or not s=0 , if we deconstruct the logic we are doing something different than normal when we apply cases (if less than, then…, else if equal…). Usually (or so we think), it is provable or determinable which of the classes we are in, so there is no difficulty. The problem is when it is not determinable which case we are in (when the general proof is instantiated on a particular example). So, I think we have to sympathise with constructivists who struggle with the idea of proof by cases in this example. The problem of provably unprovable assertions is an essential difficulty, unlike the usual examples of constuctivistically invalid proofs such as simple proofs involving excluded middle.

This really is something to think hard about, because the obvious rejoinder is not so simple as it seems. As realists, we will say, ‘Yes, but it does not matter whether we can put a given real into one or other of the cases; what matters is that we know we it is in one, so the proof is without difficulty.’ In the end, I will admit to agreeing with this obvious resolution, but the struggle is in understanding why this seems so far from the way we apply mathematical intuition. Reading the proofs in the Part II Graph Theory course, it is striking just how many proceed by cases, and how uniformly the language is phrased in a constructivist way. Now, this is a lucky course to pick because thankfully most of the things proved are determinable, so this thought paradigm works, but why do we naturally gravitate to this flawed model of polychotomy in our thinking?

Constructivism fails in the end, especially Brouwer’s intuitionism, because it cannot capture our intuition that, for example, the reals exist. If we allow ourselves to let the indeterminability of s to prevent its use in simple proofs, then it does not fulfill the (classical interpretations of) axioms for the reals, as indeed do all non-recursively enumerable elements in the reals. This is as bad as it gets really (although apparently we can safely prove IVT either with the additional condition that f is locally non-zero, or the weaker conclusion that we can find a convergent sequence xn such that f ⁡ xn → 0 ).

Constructivism stills leaves a challenge though, because it questions why the expression of our mathematical thought so frequently lines up with intuitionism, even if we are ready to reject it as soon as we have to to defend our idea of the reals, and indeed all higher mathematics.

For an interesting alternative approach, see Gowers’ A dialogue concerning the need for the real number system, Part IV.