| I think you're right on the money bringing Turing into this. I don't have a real, formal horse in this race, but the way that I have things arranged in my mind is that these are all disagreements on the notion two things in logical foundations: the need to consider time/resources and the conception of logical systems as closed or open. Brouwer and Hilbert accept that time is a factor, but handle it in different implicit ways. Hilbert differentiates between finite (time accessible) and infinite (not finite) and then makes a plea that this divide doesn't much matter. His Program sought to prove it and then Turing and Godel and the like shattered that dream. Brouwer philosophically treated proof as communication and thus Intuitionism handles time and resource naturally (though not explicitly like a Kripke model). Brouwer was forced by this choice to leave his mathematical foundations open ended as well. At any given level of effort there is a finite set of things we can prove/talk about/know and the rest must be left unknown, but likewise at any point in time we can incrementally increase our knowledge. Intuitionism is complex in order to handle that openness. Bringing Turing in makes openness and expense/time immediately obvious. Turing machines are a model for an open world of knowledge: once you have a partial halting oracle G I can build a new program which your oracle fails on. Godel took it to the next level: your own formal system cannot prove its own consistency, but using it I can create a larger universe where it can be proven consistent. In each case, the result arises from wanting a formal closure of your foundation and both use self-reference to create a (co-)inductive means of incrementally enlarging your system forever. So I think Brouwer beats them to the punch in a certain way by taking that continuous finitary expansion as foundational itself. Free choice can't be modeled formally by "Turing machines" because we possess a means for writing them all down. On the other hand, if I give you the trace of a Turing machine you have no (finite) means to predict it so "Turing machine traces" do provide the largeness you need. I don't really know how to handle the fact that someone might want to form a bijection between the two. To me it makes me think immediately of information hiding behind an abstract interface: even though you could eventually know an implementation of the interface, you spend most of your time working ignorant to it and often have more power for doing so. I'm definitely no expert here, but I think it's all really fascinating. Definitely agree that Brouwer didn't produce anything of much use to day-to-day mathematicians, but that's sort of Hilbert's (and Turing's) point: practical common sense doesn't seem too impeded by this. I think as computer scientists we're essentially carrying out a certain mathematical/philosophical program in this debate, fwiw. Turing showed that if you take working computationally very seriously that you will run into open-endedness and time-as-resource constraints very quickly. Programming is a long exercise in discovering just have very seriously you have to take both of those things (interfaces, abstraction on one side, resources, human patience on the other). Brouwer and intuitionism are subsequently having a bit of a resurgence in mechanized proving. The non-computability of reals shows its ugly head every time someone working in computational optimization has to write `compare_espilon` instead of just `equals`. Or, perhaps even better, every time someone gets bitten by thinking IEEE reals are "mathematical reals". I also really like to imagine this because I love this idea that each programmer is unknowingly taking very tiny steps along a grand philosophical program. Unromantically it's obviously true, but there's something fun in trying to imagine just how profoundly computers may yet still impact our understanding of the world. |
Well, his most famous paper, the one in he was first discovered the essence of what computation is (rather than merely asking what functions can be computed by a "definite procedure"), was named On Computable Numbers, and he uses the very problem of the real numbers as a segue into the more general topic of computation.
> Free choice can't be modeled formally by "Turing machines" because we possess a means for writing them all down. On the other hand, if I give you the trace of a Turing machine you have no (finite) means to predict it so "Turing machine traces" do provide the largeness you need. I don't really know how to handle the fact that someone might want to form a bijection between the two.
I don't think there is any such bijection (if only for the cardinality argument you mention), but that it turns out (thanks to halting), that lawful and lawless sequences are equally opaque: it is as impossible to determine (using finite means) whether two lawful sequences are equal as it is to determine whether two lawless sequences are, which is all that's required (I think) for the theory. Therefore the same idea that Brouwer had in mind does not really require lawless sequences (which, I think, he wouldn't have introduced if he'd known about halting).
> Turing showed that if you take working computationally very seriously that you will run into open-endedness and time-as-resource constraints very quickly. Programming is a long exercise in discovering just have very seriously you have to take both of those things (interfaces, abstraction on one side, resources, human patience on the other).
It's a bit more complicated, as Turing himself -- in his published conversations with Wittgenstein -- opposed intuitionism as a foundation, believing that math neither has nor requires one true formal foundation. After all, Formalism is also finitistic, and you can just as well use a program to prove a theorem about (classical) real numbers using finite means; there's no need to construct -- i.e. give specific meaning to -- each real number. That was Hilbert's point: it is enough to reason about mathematical proposition in a finitary manner, and there's no actual need to construct the objects in their domain of discourse with finitary means.
> Brouwer and intuitionism are subsequently having a bit of a resurgence in mechanized proving.
Yes, but I think the relationship is more complicated. Again, a mechanical prover can prove classical propositions -- by using deduction rules -- just as it can prove intuitionistic propositions. The resurgence with respect to mechanical provers, as far as I understand, has two reasons: 1. it is easier to create a tiny universal core for a mechanical prover based on intuitionsitic logic, and classical logic can then be built on top of that. 2. much of the research on the theory of functional programming rests on the desire (explicitly stated by Martin-Löf) to unify programming and constructive math. I personally find this approach misguided for various reasons (I'm not a mathematician or a logician, so I see this from a practicing programmer's perspective), but I can understand the appeal.
> there's something fun in trying to imagine just how profoundly computers may yet still impact our understanding of the world.
Oh, absolutely. Once Turing realized that computation is in a very strong sense a fundamental natural phenomenon, he understood the many implications (on logic, AI, biology and physics).