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