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