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
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
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
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