Having skimmed both this and, previously, Lakoff and Núñez’s book, I come away a little disappointed. It’s a very interesting discussion, to be sure, and Lakoff and Núñez bring a number of ideas to bear that are in common use although not always commonly known, but there always appears to be this speculative fantastical notion to the whole thing: it matters not what the answer it because math remains unaffected.
Lee Lady here dismisses what he considers to be Bishop’s constructivism, though I find that line of development, in particular Brouwer’s program of intuitionism, much more interesting.
As an immediate point, Intuitionism is a philosophical stance which invalidates many mathematical proofs we take for granted today as a consequence of taking a completely different view on what mathematics is. In other words, the impact of the Intuitionist’s answer to this philosophical question has tangible merit.
As computer scientists we can be quite easily sympathetic to constructivist mathematics. It feels more familiar to anyone who has lived in the Turing Tarpit for long enough; we know that we cannot escape Halting and that computation has a price—constructivism brings this awareness to mathematics. If you go too far, however, you might end up with the finitists (another philosophical stance with practical implications) but this way is dangerous because it fails to have the language to talk about limits and calculus.
(Although, if you’d like to see someone try very hard to do this while also developing a pretty wonderful theory, Jaynes' “The Logic of Science” is great.)
Intuitionists dodge this pitfall in finitist mathematics through something of a strange construction: the notion of a free choice sequence. It’s an interesting idea, perhaps best described in a reactionary position: we would like to be able to talk about mathematical objects which arise from outside of our control—perhaps through the act of communication, or perhaps if we accept Bell’s Theorem, through intrinsic otherness in reality—so we must have the language to talk about a mathematical object who’s behavior cannot be predicted. This is a free choice sequence, a constructive notion of a sequence of items from a set {A, B, C, …} going on perhaps forever but subject to no deterministic rule of which we have access.
If you can swallow choice sequences as constructive, then mathematics regains real numbers and limits. But to accept choice sequences is to accept a number of interesting consequences. For one, it appears to me that we are forced to accept that mathematics is a social or at least an explorative activity because choice sequences cannot arise within ourselves. Real numbers arise game theoretically when your counterparty retains the right to specify more detail about an argument later and provides little to no guidance as to what they may say—you are forced to account for the unknown (again, a reference to Halting) and this causes the world to become much more rich.
Perhaps more startling is the consequence that introducing choice sequences tests Church’s Thesis that all total functions are computable. This will cause immediate issue to a computer scientist because we don’t anticipate there to be something that lies between computable and not-halting, but computable things are too few to account for real numbers and so something has to give.
So all this to say, Intuitionism is interesting, you should consider looking into it if this article piques your interest!
It’s a bit tragic that the way that Lady, Lakoff, and Núñez go about explaining mathematics seems to avoid constructivism for more, to me, mystical arguments. A lot of what they balk at considering seems, today, to be well understood in fact.
My computer-scientist’s intuition tends to point me to the formalist approach. With that, all ordinary math is possible but there’s no particular getting hung-up on truth. I don’t think the constructivist approach can ever make all of the things it talks about finite. But a formalist interpretation makes it easy to say that all of that talk itself is finite and obeys rules.
As the parent says, formalism tends to not appeal to working mathematicians but suspect that’s because for the mathematician, it’s natural to believe the “thing” one deals with is important and jump from there to “real”.
“Perhaps more startling is the consequence that introducing choice sequences tests Church’s Thesis that all total functions are computable. This will cause immediate issue to a computer scientist because we don’t anticipate there to be something that lies between computable and not-halting, but computable things are too few to account for real numbers and so something has to give.”
It’s worth noting that Church’s Thesis is distinct from the Church-Turing Thesis and is a position that is rather hard to preserve once one gets to any rich logic.
Formalism is a pretty common place to wind up, I think, but it always feels like it’s solving problems by sweeping them under the rug instead of offering something useful. If you genuinely don’t care about the meaning of mathematics then you can call yourself a formalist and excuse yourself from the debate, but formalism has also come under a lot of attack depending on the exact formulation. It dodges on accounting for metamathematics and then requires metamathematical arguments to handle uncountable infinities.
So, at least in my impression, I feel that formalism is a bit of a bitter pill to swallow because it makes you aware of and dependent on processes which might be shakily non-constructive but then dodges trying to handle them.
But perhaps the real killer for me is that it doesn’t really handle any notion of the effort of verification. It’s undeniable that there are propositions which, regardless of system they are constructed within, have truth values which are not actually knowable today even if they could, by some principles, be known. Taking a dodge on this feature of the world is usually what I think of when I say that intuitionism takes into proper account the effort of mathematics and it’s something that I think anyone with algorithms experience might feel relation to.
Oh! And while that’s true about Church’s Thesis, it’s, I think, not often something people are aware of.
What I’d say is that formalism says meaning in mathematics isn’t more than what a formal process of proving, computing truth values and so-forth can give you. The provable properties of the natural numbers can be used - if you wind-up at a proposition that you know is independent, you get to choose where to say it’s true or false and then you can continue. The machinery remains correct, the only thing that’s dodged is the need to reconcile the results with a non-mathematical (“intuitive”) explanation.
It goes back to the “are numbers real” and the more general “are ideas real” questions.
The thing is that philosophy has tried to reconcile formal processes with human intuition over the last two thousand years. And this reconciliation isn’t in terms of formal correctness plus an explanation of one’s intuition, this process is in terms of formally correct plus feels-intuitively-correct (satisfies the intuitive sense of, say, meaning, etc).
The thing is that we know now that humans have tendencies to have wrong intuitions in X numbers of situations and with that understanding science broadly abandoned the reconcile and logic process and instead jumped to verifiable observations of the world (and formal deductions from those). We can see this in everything from optical illusions to persistence of any variety of delusional ideas. The Scientific Revolution replaced the intuitive position that the Sun revolves around the earth with the correct but unintuitive one but naturally a project to eliminate “intuitive” illusions is more difficult in a purely abstract realm like mathematics.
Broadly, Nietzsche and later Wittgenstein jumped to the position something that the foundational problem of meaning really were best handled in terms of psychology and linguistics rather than philosophy.
And I think one could discover a variety of interesting tendencies brought about by the way that the formalist interpretation of math rankles our intuition.
To be a formalist one must admit that formality itself at least exists in some platonic sense. If numbers don’t exist in any meaningful way but instead you merely have “propositions” and “rules”… well, what are those things? You can just apply the same trick again and treat metamathematics as meaningless manipulation of symbols, but that at least leaves a sour taste in my mouth and ends up with infinite regress problems if you keep going. I think this causes trouble for formalists.
A way of resolving the trouble is to pick up some kind of relativism and state that the rules you follow are at least semantically palatable to you. This starts to feel verificationist and I think you’ll run down intuitionism if you go this way as well. Metamathematics becomes “acceptable” when it matches the mechanism by which your mind “grasps” things and you have to be able to live atop some number of primitive, “immediate” schemata.
Or you can state that you accept formal systems which admit (P \/ not P) “just because”, I suppose. But this is that dodge I’m talking about.
There is a list of mathematics/philosophy keywords in your post that will last me a lifetime of study! I see one book there (Jayne’s) are there other you would reccommend?
Jaynes' (my mistake on the apostrophe!) Logic of Science is a good whirlwind intro to Bayesian probability theory as logic (but don’t take it too seriously as an introduction to bayesian statistics as a tool).
Intuitionism is harder to study. You can pick up a lot of it from reading about theorem provers like Coq and Agda, but you may also want to dive into it from the mathematical or philosophical perspectives. Dummet’s Elements of Intuitionism is not an easy read, but instead a powerful introduction from the mathematical/logical/philosophical side. I’ve skimmed about 90% of it and read deeply about half and it sets up an enormous research agenda were you to follow all of the loose ends within.
Edit: The SEP is also a really great resource! Here are a few links
Having skimmed both this and, previously, Lakoff and Núñez’s book, I come away a little disappointed. It’s a very interesting discussion, to be sure, and Lakoff and Núñez bring a number of ideas to bear that are in common use although not always commonly known, but there always appears to be this speculative fantastical notion to the whole thing: it matters not what the answer it because math remains unaffected.
Lee Lady here dismisses what he considers to be Bishop’s constructivism, though I find that line of development, in particular Brouwer’s program of intuitionism, much more interesting.
As an immediate point, Intuitionism is a philosophical stance which invalidates many mathematical proofs we take for granted today as a consequence of taking a completely different view on what mathematics is. In other words, the impact of the Intuitionist’s answer to this philosophical question has tangible merit.
As computer scientists we can be quite easily sympathetic to constructivist mathematics. It feels more familiar to anyone who has lived in the Turing Tarpit for long enough; we know that we cannot escape Halting and that computation has a price—constructivism brings this awareness to mathematics. If you go too far, however, you might end up with the finitists (another philosophical stance with practical implications) but this way is dangerous because it fails to have the language to talk about limits and calculus.
(Although, if you’d like to see someone try very hard to do this while also developing a pretty wonderful theory, Jaynes' “The Logic of Science” is great.)
Intuitionists dodge this pitfall in finitist mathematics through something of a strange construction: the notion of a free choice sequence. It’s an interesting idea, perhaps best described in a reactionary position: we would like to be able to talk about mathematical objects which arise from outside of our control—perhaps through the act of communication, or perhaps if we accept Bell’s Theorem, through intrinsic otherness in reality—so we must have the language to talk about a mathematical object who’s behavior cannot be predicted. This is a free choice sequence, a constructive notion of a sequence of items from a set {A, B, C, …} going on perhaps forever but subject to no deterministic rule of which we have access.
If you can swallow choice sequences as constructive, then mathematics regains real numbers and limits. But to accept choice sequences is to accept a number of interesting consequences. For one, it appears to me that we are forced to accept that mathematics is a social or at least an explorative activity because choice sequences cannot arise within ourselves. Real numbers arise game theoretically when your counterparty retains the right to specify more detail about an argument later and provides little to no guidance as to what they may say—you are forced to account for the unknown (again, a reference to Halting) and this causes the world to become much more rich.
Perhaps more startling is the consequence that introducing choice sequences tests Church’s Thesis that all total functions are computable. This will cause immediate issue to a computer scientist because we don’t anticipate there to be something that lies between computable and not-halting, but computable things are too few to account for real numbers and so something has to give.
So all this to say, Intuitionism is interesting, you should consider looking into it if this article piques your interest!
It’s a bit tragic that the way that Lady, Lakoff, and Núñez go about explaining mathematics seems to avoid constructivism for more, to me, mystical arguments. A lot of what they balk at considering seems, today, to be well understood in fact.
Actually,
My computer-scientist’s intuition tends to point me to the formalist approach. With that, all ordinary math is possible but there’s no particular getting hung-up on truth. I don’t think the constructivist approach can ever make all of the things it talks about finite. But a formalist interpretation makes it easy to say that all of that talk itself is finite and obeys rules. As the parent says, formalism tends to not appeal to working mathematicians but suspect that’s because for the mathematician, it’s natural to believe the “thing” one deals with is important and jump from there to “real”.
“Perhaps more startling is the consequence that introducing choice sequences tests Church’s Thesis that all total functions are computable. This will cause immediate issue to a computer scientist because we don’t anticipate there to be something that lies between computable and not-halting, but computable things are too few to account for real numbers and so something has to give.”
It’s worth noting that Church’s Thesis is distinct from the Church-Turing Thesis and is a position that is rather hard to preserve once one gets to any rich logic.
Formalism is a pretty common place to wind up, I think, but it always feels like it’s solving problems by sweeping them under the rug instead of offering something useful. If you genuinely don’t care about the meaning of mathematics then you can call yourself a formalist and excuse yourself from the debate, but formalism has also come under a lot of attack depending on the exact formulation. It dodges on accounting for metamathematics and then requires metamathematical arguments to handle uncountable infinities.
So, at least in my impression, I feel that formalism is a bit of a bitter pill to swallow because it makes you aware of and dependent on processes which might be shakily non-constructive but then dodges trying to handle them.
But perhaps the real killer for me is that it doesn’t really handle any notion of the effort of verification. It’s undeniable that there are propositions which, regardless of system they are constructed within, have truth values which are not actually knowable today even if they could, by some principles, be known. Taking a dodge on this feature of the world is usually what I think of when I say that intuitionism takes into proper account the effort of mathematics and it’s something that I think anyone with algorithms experience might feel relation to.
Oh! And while that’s true about Church’s Thesis, it’s, I think, not often something people are aware of.
I don’t think formalism dodges meaning.
What I’d say is that formalism says meaning in mathematics isn’t more than what a formal process of proving, computing truth values and so-forth can give you. The provable properties of the natural numbers can be used - if you wind-up at a proposition that you know is independent, you get to choose where to say it’s true or false and then you can continue. The machinery remains correct, the only thing that’s dodged is the need to reconcile the results with a non-mathematical (“intuitive”) explanation.
It goes back to the “are numbers real” and the more general “are ideas real” questions.
The thing is that philosophy has tried to reconcile formal processes with human intuition over the last two thousand years. And this reconciliation isn’t in terms of formal correctness plus an explanation of one’s intuition, this process is in terms of formally correct plus feels-intuitively-correct (satisfies the intuitive sense of, say, meaning, etc).
The thing is that we know now that humans have tendencies to have wrong intuitions in X numbers of situations and with that understanding science broadly abandoned the reconcile and logic process and instead jumped to verifiable observations of the world (and formal deductions from those). We can see this in everything from optical illusions to persistence of any variety of delusional ideas. The Scientific Revolution replaced the intuitive position that the Sun revolves around the earth with the correct but unintuitive one but naturally a project to eliminate “intuitive” illusions is more difficult in a purely abstract realm like mathematics.
Broadly, Nietzsche and later Wittgenstein jumped to the position something that the foundational problem of meaning really were best handled in terms of psychology and linguistics rather than philosophy.
And I think one could discover a variety of interesting tendencies brought about by the way that the formalist interpretation of math rankles our intuition.
To be a formalist one must admit that formality itself at least exists in some platonic sense. If numbers don’t exist in any meaningful way but instead you merely have “propositions” and “rules”… well, what are those things? You can just apply the same trick again and treat metamathematics as meaningless manipulation of symbols, but that at least leaves a sour taste in my mouth and ends up with infinite regress problems if you keep going. I think this causes trouble for formalists.
A way of resolving the trouble is to pick up some kind of relativism and state that the rules you follow are at least semantically palatable to you. This starts to feel verificationist and I think you’ll run down intuitionism if you go this way as well. Metamathematics becomes “acceptable” when it matches the mechanism by which your mind “grasps” things and you have to be able to live atop some number of primitive, “immediate” schemata.
Or you can state that you accept formal systems which admit (P \/ not P) “just because”, I suppose. But this is that dodge I’m talking about.
There is a list of mathematics/philosophy keywords in your post that will last me a lifetime of study! I see one book there (Jayne’s) are there other you would reccommend?
Jaynes' (my mistake on the apostrophe!) Logic of Science is a good whirlwind intro to Bayesian probability theory as logic (but don’t take it too seriously as an introduction to bayesian statistics as a tool).
Intuitionism is harder to study. You can pick up a lot of it from reading about theorem provers like Coq and Agda, but you may also want to dive into it from the mathematical or philosophical perspectives. Dummet’s Elements of Intuitionism is not an easy read, but instead a powerful introduction from the mathematical/logical/philosophical side. I’ve skimmed about 90% of it and read deeply about half and it sets up an enormous research agenda were you to follow all of the loose ends within.
Edit: The SEP is also a really great resource! Here are a few links
Man I got a kick out of that.
Thanks for the post, I greatly enjoyed reading this. :)
Of course they do, anyone who’s ever watched Sesame Street knows that!