Logic poking holes in classical maths; challenge to solve

I would like to expand a bit more on one of last week’s posts because it is really not clear what the right answer is. Paul Taylor (A lambda calculus for real analysis, <http://paultaylor.eu/ASD/lamcra/>) develops a lambda-like calculus for reasoning computationally about topology. This is very interesting and throws out some quirky results.

This example starts off as a curiosity but raises some important questions. Begin with

g n = { 1 if n encodes a proof that 0 = 1 0 otherwise,

of which we know by Gödel (second theorem) the values are unknowable, provided we allow ourselves a sensible proportion of Peano arithmetic. So, we can construct a simple constant s = 2 - n g n to produce some interesting problems.

You see, what we often forget when thinking about logic is that we actually use it to build everything else up. When we take these awkward numbers and start using them in analysis, the difficulties on the bottom are not just of interest to logicians.

What I would like to know is this: is there an easy way to show that even a simple function like f x = x + s has a root? (Not obvious.) All the standard proofs, whether by bisection, limits, the lot, assume you can do some pretty basic things like determine the order between two real numbers, whereas in fact that might be provably impossible.

This sort of problem was attacked by Brouwer, who focussed on the philosophical side (it seems) of quantities which may be determined but are currently unknown. On this basis he developed his constructivism, which I used to be extremely unsympathetic to on the grounds that things which are essentially parameters, though practically different to ordinary real numbers, and theoretically the same. The sort of repercussions of logical difficulties like the example here were only realised later, and I think give a much stronger impetus to that school of thought. In the end, I still am firmly not an intuitionist philosophically, but at least now find these sorts of problems very much more relevant.

So, any takers? Can functions like f in general be said to have a root? Or, are we in a situation like in set theory where our working universe is smaller than the meta-universe, and s which exists in the meta-world is a ‘hole’ on the real line in the working world?