Second-order logic is not part of standard, mainstream mathematics. It is part of a field that you might call mathematical logic or “foundations of mathematics”. Foundations of a building are relevant to the strength of a building, so the name implies that foundations of mathematics are relevant to the strength of mainstream mathematics. A more accurate analogy would be the relationship between physics and philosophy of physics—discoveries in epistemology and philosophy of science are more often driven by physics than the other way around, and the field “philosophy of physics” is a backwater by comparison.
As is probably evident, I think the good, solid mathematical logic is intuitionist and constructive and higher-order and based on proof theory first and model theory only second. It is easy to analogize from their names to a straight line between first-order, second-order, and higher-order logic, but in fact they’re not in a straight line at all. First-order logic is mainstream mathematics, second-order logic is mathematical logic flavored with faith in the reality of infinite models and set theory, and higher-order logic is mathematical logic that is (usually) constructive and proof-theoretic and built with an awareness of computer science.
To an extent, but I think it’s obvious that most mathematicians couldn’t care less whether or not their theorems are expressible in second-order logic.
Yes, because most mathematicians just take SOL at face value. If you believe in SOL and use the corresponding English language in your proofs—i.e., you assume there’s only one field of real numbers and you can talk about it—then of course it doesn’t matter to you whether or not your theorem happens to require SOL taken at face value, just like it doesn’t matter to you whether your proof uses ~~P->P as a logical axiom. Only those who distrust SOL would try to avoid proofs that use it. That most mathematicians don’t care is precisely how we know that disbelief in SOL is not a mainstream value. :)
The standard story is that everything mathematicians prove is to be interpreted as a statement in the language of ZFC, with ZFC itself being interpreted in first-order logic. (With a side-order of angsting about how to talk about e.g. “all” vector spaces, since there isn’t a set containing all of them—IMO there are various good ways of resolving this, but the standard story considers it a problem; certainly in so far as SOL provides an answer to these concerns at all, it’s not “the one” answer that everybody is obviously implicitly using.) So when they say that there’s only one field of real numbers, this is supposed to mean that you can formalize the field axioms as a ZFC predicate about sets, and then prove in ZFC that between any two sets satisfying this predicate, there is an isomorphism. The fact that the semantics of first-order logic don’t pin down a unique model of ZFC isn’t seen as conflicting with this; the mathematician’s statement that there is only one complete ordered field (up to isomorphism) is supposed to desugar to a formal statement of ZFC, or more precisely to the meta-assertion that this formal statement can be proven from the ZFC axioms. Mathematical practice seems to me more in line with this story than with yours, e.g. mathematicians find nothing strange about introducing the reals through axioms and then talk about a “neighbourhood basis” as something that assigns to each real number a set of sets of real numbers—you’d need fourth-order logic if you wanted to talk about neighbourhood bases as objects without having some kind of set theory in the background. And people who don’t seem to care a fig about logic will use Zorn’s lemma when they want to prove something that uses choice, which seems quite rooted in set theory.
Now I do think that mathematicians think of the objects they’re discussing as more “real” than the standard story wants them to, and just using SOL instead of FOL as the semantics in which we interpret the ZFC axioms would be a good way to, um, tell a better story—I really like your post and it has convinced me of the usefulness of SOL—but I think if we’re simply trying to describe how mathematicians really think about what they’re doing, it’s fairer to say that they’re just taking set theory at face value—not thinking of set theory as something that has axioms that you formalize in some logic, but seeing it as as fundamental as logic itself, more or less.
Um, I think when an ordinary mathematician says that there’s only one complete ordered field up to isomorphism, they do not mean, “In any given model of ZFC, of which there are many, there’s only one ordered field complete with respect to the predicates for which sets exist in that model.” We could ask some normal mathematicians what they mean to test this. We could also prove the isomorphism using logic that talked about all predicates, and ask them if they thought that was a fair proof (without calling attention to the quantification over predicates).
Taking set theory at face value is taking SOL at face value—SOL is often seen as importing set theory into logic, which is why mathematicians who care about it all are sometimes suspicious of it.
Um, I think when an ordinary mathematician says that there’s only one complete ordered field up to isomorphism, they do not mean, “In any given model of ZFC, of which there are many, there’s only one ordered field complete with respect to the predicates for which sets exist in that model.” We could ask some normal mathematicians what they mean to test this.
The standard story, as I understand it, is claiming that models don’t even enter into it; the ordinary mathematician is supposed to be saying only that the corresponding statement can be proven in ZFC. Of course, that story is actually told by logicians, not by people who learned about models in their one logic course and then promptly forgot about them after the exam. As I said, I don’t agree with the standard story as a fair characterization of what mathematicians are doing who don’t care about logic. (Though I do think it’s a coherent story about what the informal mathematical English is supposed to mean.)
Taking set theory at face value is taking SOL at face value—SOL is often seen as importing set theory into logic, which is why mathematicians who care about it all are sometimes suspicious of it.
Is it a fair-rephrasing of your point that what normal mathematicians do requires the same order of ontological commitment as the standard (non-Henkin) semantics of SOL, since if you take SOL as primitive and interpret the ZFC axioms in it, that will give you the correct powerset of the reals, and if you take set theory as primitive and formalize the semantics of SOL in it, you will get the correct collection of standard models? ’Cause I agree with that (and I see the value of SOL as a particularly simple way of making that ontological commitment, compared to say ZFC). My point was that mathematical English maps much more directly to ZFC than it does to SOL (there’s still coding to be done, but much less of it when you start from ZFC than when you start from SOL); e.g., you earlier said that “[o]nly those who distrust SOL would try to avoid proofs that use it”, and you can’t really use ontological commitments in proofs, what you can actually use is notions like “for all properties of real numbers”, and many notions people actually use are ones more directly present in ZFC than SOL, like my example of quantifying over the neighbourhood bases (mappings from reals to sets of sets of reals).
So to take your example of real numbers—if someone didn’t want to use SOL, they would still prove the same theorems, they would just end up proving that they are true for any Archimedean complete totally ordered field. In general, I think most mathematics (i.e. mathematics outside set theory and logic) is robust with respect to foundations: rarely is it the case that a change in axioms makes a proof invalid, it just means you’re talking about something slightly different. The idea of the proof is still preserved.
I agree with this statement—and yet you did not contradict my statement that second order logic is also not part of mainstream mathematics.
A topologist might care about manifolds or homeomorphisms—they do not care about foundations of mathematics—and it is not the case that only one foundation of mathematics can support topology. The weaker foundation is preferable.
The last sentence is not obvious at all. The goal of mathematics is not to be correct a lot. The goal of mathematics is to promote human understanding. Strong axioms help with that by simplifying reasoning.
If you assume A and derive B you have not proven B but rather A implies B. If you can instead assume a weaker axiom Aprime, and still derive B, then you have proven Aprime implies B, which is stronger because it will be applicable in more circumstances.
If you were writing software for something intended to traverse the Interplanetary transfer network then you would probably use charts and atlases and transition functions, and you would study (symplectic) manifolds and homeomorphisms in order to understand those more-applied concepts.
If an otherwise useful theorem assumes that the manifold is orientable, then you need to show that your practical manifold is orientable before you can use it—and if it turns out not to be orientable, then you can’t use it at all. If instead you had an analogous theorem that applied to all manifolds, then you could use it immediately.
There’s a difference between assuming that a manifold is orientable and assuming something about set theory. The phase space is, of course, only approximately a manifold. On a very small level it’s—well, something we’re not very sure of. But all the math you’ll be doing is an approximation of reality.
So some big macroscopic feature like orientability would be a problem to assume. Orientability corresponds to something in physical reality, and something that clearly matters for your calculation.
The axiom of choice or whatever set-theoretic assumption corresponds to nothing in physical reality. It doesn’t matter if the theorems you are using are right for the situation, because they are obviously all wrong, because they are about symplectic dynamics on a manifold, and physics isn’t actually symplectic dynamics on a manifold! The only thing that matters is how easily you can find a good-enough approximation to reality. More foundational assumptions make this easier, and do not impede one’s approximation of reality.
Note that physicists frequently make arguments that are just plain unambiguously wrong from a mathematical perspective.
I understand your point—it’s akin to the Box quote “all models are wrong but some are useful”—when choosing among (false) models, choose the most useful one. However, it is not the case that stronger assumptions are more useful—of course stronger assumptions make the task of proving easier, but the task as a whole includes both proving and also building a system based on the theorems proven.
My primary point is that EY is implying that second-order logic is necessary to work with the integers. People work with the integers without using second-order logic all the time. If he said that he is only introducing second-order logic for convenience in proving and there are certainly other ways of doing it, and that some people (intuitionists and finitists) think that introducing second-order logic is a dubious move, I’d be happy.
My other claim that second-order logic is unphysical and that its unphysicality probably does ripple out to make practical tasks more difficult, is a secondary one. I’m happy to agree that this secondary claim is not mainstream.
My primary point is actually that I don’t care if math is useful. Math is awesome. This is obviously an extremely rare viewpoint, but very common among.
But I do agree with that quote, more or less. I think that potentially some models are true, but those models are almost certainly less useful for most purposes than the crude and easy to work with approximations.
I agree that second-order logic is not necessary to work with the integers. Second-order logic is necessary to work with the integers and only the integers, however. Somewhat problematically, it’s not actually possible to work with second-order logic.
Second-order logic is not part of standard, mainstream mathematics. It is part of a field that you might call mathematical logic or “foundations of mathematics”. Foundations of a building are relevant to the strength of a building, so the name implies that foundations of mathematics are relevant to the strength of mainstream mathematics. A more accurate analogy would be the relationship between physics and philosophy of physics—discoveries in epistemology and philosophy of science are more often driven by physics than the other way around, and the field “philosophy of physics” is a backwater by comparison.
As is probably evident, I think the good, solid mathematical logic is intuitionist and constructive and higher-order and based on proof theory first and model theory only second. It is easy to analogize from their names to a straight line between first-order, second-order, and higher-order logic, but in fact they’re not in a straight line at all. First-order logic is mainstream mathematics, second-order logic is mathematical logic flavored with faith in the reality of infinite models and set theory, and higher-order logic is mathematical logic that is (usually) constructive and proof-theoretic and built with an awareness of computer science.
Your view is not mainstream.
To an extent, but I think it’s obvious that most mathematicians couldn’t care less whether or not their theorems are expressible in second-order logic.
Yes, because most mathematicians just take SOL at face value. If you believe in SOL and use the corresponding English language in your proofs—i.e., you assume there’s only one field of real numbers and you can talk about it—then of course it doesn’t matter to you whether or not your theorem happens to require SOL taken at face value, just like it doesn’t matter to you whether your proof uses ~~P->P as a logical axiom. Only those who distrust SOL would try to avoid proofs that use it. That most mathematicians don’t care is precisely how we know that disbelief in SOL is not a mainstream value. :)
The standard story is that everything mathematicians prove is to be interpreted as a statement in the language of ZFC, with ZFC itself being interpreted in first-order logic. (With a side-order of angsting about how to talk about e.g. “all” vector spaces, since there isn’t a set containing all of them—IMO there are various good ways of resolving this, but the standard story considers it a problem; certainly in so far as SOL provides an answer to these concerns at all, it’s not “the one” answer that everybody is obviously implicitly using.) So when they say that there’s only one field of real numbers, this is supposed to mean that you can formalize the field axioms as a ZFC predicate about sets, and then prove in ZFC that between any two sets satisfying this predicate, there is an isomorphism. The fact that the semantics of first-order logic don’t pin down a unique model of ZFC isn’t seen as conflicting with this; the mathematician’s statement that there is only one complete ordered field (up to isomorphism) is supposed to desugar to a formal statement of ZFC, or more precisely to the meta-assertion that this formal statement can be proven from the ZFC axioms. Mathematical practice seems to me more in line with this story than with yours, e.g. mathematicians find nothing strange about introducing the reals through axioms and then talk about a “neighbourhood basis” as something that assigns to each real number a set of sets of real numbers—you’d need fourth-order logic if you wanted to talk about neighbourhood bases as objects without having some kind of set theory in the background. And people who don’t seem to care a fig about logic will use Zorn’s lemma when they want to prove something that uses choice, which seems quite rooted in set theory.
Now I do think that mathematicians think of the objects they’re discussing as more “real” than the standard story wants them to, and just using SOL instead of FOL as the semantics in which we interpret the ZFC axioms would be a good way to, um, tell a better story—I really like your post and it has convinced me of the usefulness of SOL—but I think if we’re simply trying to describe how mathematicians really think about what they’re doing, it’s fairer to say that they’re just taking set theory at face value—not thinking of set theory as something that has axioms that you formalize in some logic, but seeing it as as fundamental as logic itself, more or less.
Um, I think when an ordinary mathematician says that there’s only one complete ordered field up to isomorphism, they do not mean, “In any given model of ZFC, of which there are many, there’s only one ordered field complete with respect to the predicates for which sets exist in that model.” We could ask some normal mathematicians what they mean to test this. We could also prove the isomorphism using logic that talked about all predicates, and ask them if they thought that was a fair proof (without calling attention to the quantification over predicates).
Taking set theory at face value is taking SOL at face value—SOL is often seen as importing set theory into logic, which is why mathematicians who care about it all are sometimes suspicious of it.
The standard story, as I understand it, is claiming that models don’t even enter into it; the ordinary mathematician is supposed to be saying only that the corresponding statement can be proven in ZFC. Of course, that story is actually told by logicians, not by people who learned about models in their one logic course and then promptly forgot about them after the exam. As I said, I don’t agree with the standard story as a fair characterization of what mathematicians are doing who don’t care about logic. (Though I do think it’s a coherent story about what the informal mathematical English is supposed to mean.)
Is it a fair-rephrasing of your point that what normal mathematicians do requires the same order of ontological commitment as the standard (non-Henkin) semantics of SOL, since if you take SOL as primitive and interpret the ZFC axioms in it, that will give you the correct powerset of the reals, and if you take set theory as primitive and formalize the semantics of SOL in it, you will get the correct collection of standard models? ’Cause I agree with that (and I see the value of SOL as a particularly simple way of making that ontological commitment, compared to say ZFC). My point was that mathematical English maps much more directly to ZFC than it does to SOL (there’s still coding to be done, but much less of it when you start from ZFC than when you start from SOL); e.g., you earlier said that “[o]nly those who distrust SOL would try to avoid proofs that use it”, and you can’t really use ontological commitments in proofs, what you can actually use is notions like “for all properties of real numbers”, and many notions people actually use are ones more directly present in ZFC than SOL, like my example of quantifying over the neighbourhood bases (mappings from reals to sets of sets of reals).
So to take your example of real numbers—if someone didn’t want to use SOL, they would still prove the same theorems, they would just end up proving that they are true for any Archimedean complete totally ordered field. In general, I think most mathematics (i.e. mathematics outside set theory and logic) is robust with respect to foundations: rarely is it the case that a change in axioms makes a proof invalid, it just means you’re talking about something slightly different. The idea of the proof is still preserved.
I agree with this statement—and yet you did not contradict my statement that second order logic is also not part of mainstream mathematics.
A topologist might care about manifolds or homeomorphisms—they do not care about foundations of mathematics—and it is not the case that only one foundation of mathematics can support topology. The weaker foundation is preferable.
The last sentence is not obvious at all. The goal of mathematics is not to be correct a lot. The goal of mathematics is to promote human understanding. Strong axioms help with that by simplifying reasoning.
If you assume A and derive B you have not proven B but rather A implies B. If you can instead assume a weaker axiom Aprime, and still derive B, then you have proven Aprime implies B, which is stronger because it will be applicable in more circumstances.
In what “circumstances” are manifolds and homeomorphisms useful?
If you were writing software for something intended to traverse the Interplanetary transfer network then you would probably use charts and atlases and transition functions, and you would study (symplectic) manifolds and homeomorphisms in order to understand those more-applied concepts.
If an otherwise useful theorem assumes that the manifold is orientable, then you need to show that your practical manifold is orientable before you can use it—and if it turns out not to be orientable, then you can’t use it at all. If instead you had an analogous theorem that applied to all manifolds, then you could use it immediately.
There’s a difference between assuming that a manifold is orientable and assuming something about set theory. The phase space is, of course, only approximately a manifold. On a very small level it’s—well, something we’re not very sure of. But all the math you’ll be doing is an approximation of reality.
So some big macroscopic feature like orientability would be a problem to assume. Orientability corresponds to something in physical reality, and something that clearly matters for your calculation.
The axiom of choice or whatever set-theoretic assumption corresponds to nothing in physical reality. It doesn’t matter if the theorems you are using are right for the situation, because they are obviously all wrong, because they are about symplectic dynamics on a manifold, and physics isn’t actually symplectic dynamics on a manifold! The only thing that matters is how easily you can find a good-enough approximation to reality. More foundational assumptions make this easier, and do not impede one’s approximation of reality.
Note that physicists frequently make arguments that are just plain unambiguously wrong from a mathematical perspective.
I understand your point—it’s akin to the Box quote “all models are wrong but some are useful”—when choosing among (false) models, choose the most useful one. However, it is not the case that stronger assumptions are more useful—of course stronger assumptions make the task of proving easier, but the task as a whole includes both proving and also building a system based on the theorems proven.
My primary point is that EY is implying that second-order logic is necessary to work with the integers. People work with the integers without using second-order logic all the time. If he said that he is only introducing second-order logic for convenience in proving and there are certainly other ways of doing it, and that some people (intuitionists and finitists) think that introducing second-order logic is a dubious move, I’d be happy.
My other claim that second-order logic is unphysical and that its unphysicality probably does ripple out to make practical tasks more difficult, is a secondary one. I’m happy to agree that this secondary claim is not mainstream.
My primary point is actually that I don’t care if math is useful. Math is awesome. This is obviously an extremely rare viewpoint, but very common among.
But I do agree with that quote, more or less. I think that potentially some models are true, but those models are almost certainly less useful for most purposes than the crude and easy to work with approximations.
I agree that second-order logic is not necessary to work with the integers. Second-order logic is necessary to work with the integers and only the integers, however. Somewhat problematically, it’s not actually possible to work with second-order logic.
What sort of practical tasks are you thinking of?