6 ms·

With all due respect to physicists and their work, physics doesn't belong in the foundation of mathematics. If our understanding of physics changed drastically

With all due respect to physicists and their work, physics doesn't belong in the foundation of mathematics. If our understanding of physics changed drastically tomorrow (an admittedly very improbable event), all mathematics not directly related to physics should remain unaffected. On the other hand, computation does belong in the foundations: constructing and verifying proofs (even informal ones) is computing, and it is the role of foundations to tell us how those computations can be carried out in a pleasant way. Any change in our understanding of computation should lead us to revise how we construct and verify proofs.

pron 10y ago
But the definition of computation is physical. The Church-Turing thesis is a physical hypothesis. It is conceivable that a new physical discovery will contradict the Church-Turing thesis, and with it the definition of what is computable (and in particular how we construct and verify proofs, which is but a small part of computation).
- catnaroek 10y ago
  > But the definition of computation is physical. A lot of mathematics is inspired by physical considerations, but mathematical concepts are themselves not physical. In particular, computation is just having state transitions, not necessarily in a physical system. (Just like recursion is any form of self-reference in any definition, not necessarily procedure definitions.) > The Church-Turing thesis is a physical hypothesis. Then let's not mention it, and stick to what can be dealt with mathematically.
  - pron 10y ago
    > A lot of mathematics is inspired by physical considerations, but mathematical concepts are themselves not physical. I'm not sure I understand your point. It is true that any computation can be modeled mathematically, but so can any other physical process. Also, computation does not require a specific physical implementation and is an abstract concept, but so what? Gödel, Turing and von Neumann were very well aware that computation is a physical/philosophical concept described mathematically, not a purely mathematical one. > Then let's not mention it, and stick to what can be dealt with mathematically. But the definition of what is computable and what isn't depends on the Church-Turing thesis.
- eastWestMath 10y ago
  Computation is an entirely abstract thing. Nowhere does the definition of Turing machines or the lambda calculus makes any reference to actual physical things.
  - pron 10y ago
    Church doesn't really define computation[1], and Turing most certainly bases his entire definition (the first ever definition of computation) on multiple references to physical things (finite "states of mind", limits of what can be read or manipulated at any one time etc.). Brouwer also bases intuitionism on the physical, when he appeals to the limited capability of a finite (idealized) mind. Computation carried out with an infinitely fast (in terms of physical time) and/or infinitely large computer is not Turing computation. [1]: He conjectures that LC coincides with what he calls a "a vague intuitive notion" of an algorithm, and when he tries to make a rigorous argument he finds that he needs to rely on circularity, and writes this: "if this [circular] interpretation or some similar one is not allowed, it is difficult to see how the notion of an algorithm can be given any exact meaning at all."
    - fmap 10y ago
      Can you link to some of the references you cite? That seems like an interesting read. As for computability being a physical notion, I can't speak to the motivation of Church and his students, but I do know that there are characterizations of total computable functions in domain theory which make no mention of physics. The intuition about computable functions is that they are precisely the functions whose output for any given input depends only on a finite part of the input. The really interesting thing about the Church Turing thesis is that there are so many different models of computation that capture precisely this idea (the surprising part is that these very simple models are expressive enough to cover all computable functions).
      - pron 10y ago
        > Can you link to some of the references you cite? That seems like an interesting read. Sure. It's best to start with Jean van Heijenoort's seminal From Frege to Gödel A Source Book in Mathematical Logic, 1879-1931[1]. It includes the original texts by Hilbert, Brouwer and many others, but the text I personally found most interesting was Hermann Weyl's, which I quoted here[2] nearly in full (in the parent comment I quoted some relevant passages from Brouwer and Hilbert; in fact, it was as part of that Reddit discussion that I found the references and learned what little I know of the philosophy of mathematics). I've also found Juliet's Floyd's discussion of Turing's (and Wittgenstein's) mathematical philosophy[3] fascinating. She pinpoints how and why Turing viewed the philosophy of mathematics the way he did, how that view led him to the discovery of computation, and why people like Gödel and others found that to be such a profound philosophical breakthrough. The Stanford Encyclopedia of Philosophy's entry on the philosophy of mathematics gives a good overview[4]. > The intuition about computable functions is that they are precisely the functions whose output for any given input depends only on a finite part of the input. Once you know what computation is, you can define it in many ways. But why would that definition coincide with what we call computation? You can define foo to be such functions, but why are you calling them computable? And, BTW, even the very definition of finite possibly (I'm not sure about this point) requires reliance on the physical due to the multiple models of FOL and the problems with SOL. > The really interesting thing about the Church Turing thesis is that there are so many different models of computation that capture precisely this idea It is absolutely trivial to come up with a super-Turing mathematical model (e.g. just use reals, as in "pick the supremum of this bounded set of reals", or use a Turing machine with an infinite number of heads). All those other models are somehow based on capturing an intuitive notion of the human thought process, which is completely physical, and therefore, it is not surprising that they coincide. Turing was just the first who was able to give the notion a precise mathematical meaning. If you go back to the inception of those ideas, from Brouwer's intuitionism, Hilbert's formalism and even to the far older notion of the algorithm, you see that they're all tied to the capabilities of a physical human mind. It's true that not all of those ideas actually mention physics because not all thinkers necessarily believed the mind to be completely physical, but they're all based on the idea of a limited mind, which I think we can safely call physical. [1]: http://www.hup.harvard.edu/catalog.php?isbn=9780674324497 http://www.hup.harvard.edu/catalog.php?isbn=9780674324497 [2]: https://www.reddit.com/r/programming/comments/5k1v04/is_mathematics_the_oldest_legacy_system/dbv2gz6/ https://www.reddit.com/r/programming/comments/5k1v04/is_math... [3]: https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf [4]: https://plato.stanford.edu/entries/philosophy-mathematics/ https://plato.stanford.edu/entries/philosophy-mathematics/
AnimalMuppet 10y ago
> constructing and verifying proofs (even informal ones) is computing I'd like to see your proof for that assertion...

pron 10y ago

But the definition of computation is physical. The Church-Turing thesis is a physical hypothesis. It is conceivable that a new physical discovery will contradict the Church-Turing thesis, and with it the definition of what is computable (and in particular how we construct and verify proofs, which is but a small part of computation).

catnaroek 10y ago
> But the definition of computation is physical. A lot of mathematics is inspired by physical considerations, but mathematical concepts are themselves not physical. In particular, computation is just having state transitions, not necessarily in a physical system. (Just like recursion is any form of self-reference in any definition, not necessarily procedure definitions.) > The Church-Turing thesis is a physical hypothesis. Then let's not mention it, and stick to what can be dealt with mathematically.
- pron 10y ago
  > A lot of mathematics is inspired by physical considerations, but mathematical concepts are themselves not physical. I'm not sure I understand your point. It is true that any computation can be modeled mathematically, but so can any other physical process. Also, computation does not require a specific physical implementation and is an abstract concept, but so what? Gödel, Turing and von Neumann were very well aware that computation is a physical/philosophical concept described mathematically, not a purely mathematical one. > Then let's not mention it, and stick to what can be dealt with mathematically. But the definition of what is computable and what isn't depends on the Church-Turing thesis.
eastWestMath 10y ago
Computation is an entirely abstract thing. Nowhere does the definition of Turing machines or the lambda calculus makes any reference to actual physical things.
- pron 10y ago
  Church doesn't really define computation[1], and Turing most certainly bases his entire definition (the first ever definition of computation) on multiple references to physical things (finite "states of mind", limits of what can be read or manipulated at any one time etc.). Brouwer also bases intuitionism on the physical, when he appeals to the limited capability of a finite (idealized) mind. Computation carried out with an infinitely fast (in terms of physical time) and/or infinitely large computer is not Turing computation. [1]: He conjectures that LC coincides with what he calls a "a vague intuitive notion" of an algorithm, and when he tries to make a rigorous argument he finds that he needs to rely on circularity, and writes this: "if this [circular] interpretation or some similar one is not allowed, it is difficult to see how the notion of an algorithm can be given any exact meaning at all."
  - fmap 10y ago
    Can you link to some of the references you cite? That seems like an interesting read. As for computability being a physical notion, I can't speak to the motivation of Church and his students, but I do know that there are characterizations of total computable functions in domain theory which make no mention of physics. The intuition about computable functions is that they are precisely the functions whose output for any given input depends only on a finite part of the input. The really interesting thing about the Church Turing thesis is that there are so many different models of computation that capture precisely this idea (the surprising part is that these very simple models are expressive enough to cover all computable functions).
    - pron 10y ago
      > Can you link to some of the references you cite? That seems like an interesting read. Sure. It's best to start with Jean van Heijenoort's seminal From Frege to Gödel A Source Book in Mathematical Logic, 1879-1931[1]. It includes the original texts by Hilbert, Brouwer and many others, but the text I personally found most interesting was Hermann Weyl's, which I quoted here[2] nearly in full (in the parent comment I quoted some relevant passages from Brouwer and Hilbert; in fact, it was as part of that Reddit discussion that I found the references and learned what little I know of the philosophy of mathematics). I've also found Juliet's Floyd's discussion of Turing's (and Wittgenstein's) mathematical philosophy[3] fascinating. She pinpoints how and why Turing viewed the philosophy of mathematics the way he did, how that view led him to the discovery of computation, and why people like Gödel and others found that to be such a profound philosophical breakthrough. The Stanford Encyclopedia of Philosophy's entry on the philosophy of mathematics gives a good overview[4]. > The intuition about computable functions is that they are precisely the functions whose output for any given input depends only on a finite part of the input. Once you know what computation is, you can define it in many ways. But why would that definition coincide with what we call computation? You can define foo to be such functions, but why are you calling them computable? And, BTW, even the very definition of finite possibly (I'm not sure about this point) requires reliance on the physical due to the multiple models of FOL and the problems with SOL. > The really interesting thing about the Church Turing thesis is that there are so many different models of computation that capture precisely this idea It is absolutely trivial to come up with a super-Turing mathematical model (e.g. just use reals, as in "pick the supremum of this bounded set of reals", or use a Turing machine with an infinite number of heads). All those other models are somehow based on capturing an intuitive notion of the human thought process, which is completely physical, and therefore, it is not surprising that they coincide. Turing was just the first who was able to give the notion a precise mathematical meaning. If you go back to the inception of those ideas, from Brouwer's intuitionism, Hilbert's formalism and even to the far older notion of the algorithm, you see that they're all tied to the capabilities of a physical human mind. It's true that not all of those ideas actually mention physics because not all thinkers necessarily believed the mind to be completely physical, but they're all based on the idea of a limited mind, which I think we can safely call physical. [1]: http://www.hup.harvard.edu/catalog.php?isbn=9780674324497 http://www.hup.harvard.edu/catalog.php?isbn=9780674324497 [2]: https://www.reddit.com/r/programming/comments/5k1v04/is_mathematics_the_oldest_legacy_system/dbv2gz6/ https://www.reddit.com/r/programming/comments/5k1v04/is_math... [3]: https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf [4]: https://plato.stanford.edu/entries/philosophy-mathematics/ https://plato.stanford.edu/entries/philosophy-mathematics/

AnimalMuppet 10y ago

> constructing and verifying proofs (even informal ones) is computing I'd like to see your proof for that assertion...