3 ms·

The usual objection, which I happen to agree with, is that this is a false tradeoff. The two are inextricably linked. In the case of second-order logic, althou

The usual objection, which I happen to agree with, is that this is a false tradeoff. The two are inextricably linked. In the case of second-order logic, although it seems like we're getting a precise, single semantic model, in fact all we've done is push the ambiguity to the metatheory which we use to interpret the semantics of second-order logic. For example, there's the infamous "CH statement" of second-order logic, which has a model if and only if the Continuum Hypothesis holds in the metatheory. I mean sure that's precision if you believe that the Continuum Hypothesis has an absolute truth value (that is you can confidently say "yes CH is true/false in reality") but that's really just the same thing to me at the end of the day as choosing a particular model for a first-order theory and saying "yes that model is the one true model" (which I don't really philosophically agree with in the first place since I'm usually not a strong Platonist). Even the choice to use full semantics instead of Henkin semantics (an example of what is essentially multi-sorted FOL as @pron refers to) is an ambiguous choice one must make in deciding second-order semantics.

pdonis 6y ago
> In the case of second-order logic, although it seems like we're getting a precise, single semantic model, in fact all we've done is push the ambiguity to the metatheory which we use to interpret the semantics of second-order logic. So how would this work in, say, the case of the natural numbers? What ambiguity gets pushed to the metatheory if I claim that the second order theory of the natural numbers pins down a single semantic model (the "standard" natural numbers and that's all)? If it matters, assume we are using full semantics, not Henkin semantics (see further comments on that below). > Even the choice to use full semantics instead of Henkin semantics (an example of what is essentially multi-sorted FOL as @pron refers to) is an ambiguous choice one must make in deciding second-order semantics. I'm not sure I would call this choice "ambiguous" since the difference between the two choices is perfectly clear, and only one of them (full semantics) preserves the key property of second order logic, of pinning down a single semantic model.
- dwohnitmok 6y ago
  Caveat: All of this is essentially philosophy at this point and so there's no rigorous argument I can present that second-order logic is wrong. But I think you've asked reasonable questions so let's dive in. So the CH statement (let's call it CH_2 where 2 is for second-order) I was referring to actually uses the empty vocabulary (i.e. only the usual symbols from second-order logic). In particular that means it also applies to second-order Peano Arithmetic. So does your model of the natural numbers satisfy CH_2 or not (or put differently, is your proposed model of the natural numbers actually a model of the natural numbers)? Depends on your metatheory. More problematically, what this demonstrates (because CH is independent of ZFC) is that second-order logic loses the absoluteness of semantic truth. That is the statement "M is a model of my theory T under a given interpretation I" can flip-flop between true and false and back again as you continue to expand your background model of your metatheory (think of e.g. Cohen forcing). So while you may have specified exactly one model, it's getting pretty hard to see just exactly which one it is. First-order logic does not have this phenomenon, which is why we can often get away with not going into too much detail about our metatheory in FOL (and why recursive metatheories built of FOL "all the way down" aren't too problematic). If M is a model of T under I then it will continue to be a model of T under expansion of my background model. So as long as I sketch out the basics of my metatheory (and by implication my background model), I know I'm good. Philosophically this means that in the realm of SOL the only way you can be sure that you've really got "the" standard model and haven't mistakenly grabbed another one is if you can confidently state the truth value of every one of a never-ending stream of theorems which cannot be proved using your metatheory. Indeed statements like "Theorem A is independent of theory T" are very murky and difficult to understand in a second-order setting. For example, CH_2 is definitely not provable using second-order PA, but does that mean we can accept systems with either CH_2 or Not(CH_2)? Well that seems to be false if we take "a single canonical model" at face value, which would imply that only one of the two can be "true," but then how do you decide whether to accept CH_2 or Not(CH_2)? No syntactic argument will suffice since we've lost completeness. That's not to say I think that second-order logic has no value. I think second-order logic, interpreted using first-order semantics, is a valuable language. However, I agree very much with Vaananen's contention that in practice, SOL reduces to multi-sorted FOL. > if second-order logic is used in formalizing or axiomatizing mathematics, the choice of semantics is irrelevant: it cannot meaningfully be asked whether one should use Henkin semantics or full semantics. This question arises only if we formalize second-order logic after we have formalized basic mathematical concepts needed for semantics. A choice between the Henkin second-order logic and the full second-order logic as a primary formalization of mathematics cannot be made; they both come out the same. http://www.math.helsinki.fi/logic/people/jouko.vaananen/VaaSec.pdf http://www.math.helsinki.fi/logic/people/jouko.vaananen/VaaS...

pdonis 6y ago

> In the case of second-order logic, although it seems like we're getting a precise, single semantic model, in fact all we've done is push the ambiguity to the metatheory which we use to interpret the semantics of second-order logic. So how would this work in, say, the case of the natural numbers? What ambiguity gets pushed to the metatheory if I claim that the second order theory of the natural numbers pins down a single semantic model (the "standard" natural numbers and that's all)? If it matters, assume we are using full semantics, not Henkin semantics (see further comments on that below). > Even the choice to use full semantics instead of Henkin semantics (an example of what is essentially multi-sorted FOL as @pron refers to) is an ambiguous choice one must make in deciding second-order semantics. I'm not sure I would call this choice "ambiguous" since the difference between the two choices is perfectly clear, and only one of them (full semantics) preserves the key property of second order logic, of pinning down a single semantic model.

dwohnitmok 6y ago
Caveat: All of this is essentially philosophy at this point and so there's no rigorous argument I can present that second-order logic is wrong. But I think you've asked reasonable questions so let's dive in. So the CH statement (let's call it CH_2 where 2 is for second-order) I was referring to actually uses the empty vocabulary (i.e. only the usual symbols from second-order logic). In particular that means it also applies to second-order Peano Arithmetic. So does your model of the natural numbers satisfy CH_2 or not (or put differently, is your proposed model of the natural numbers actually a model of the natural numbers)? Depends on your metatheory. More problematically, what this demonstrates (because CH is independent of ZFC) is that second-order logic loses the absoluteness of semantic truth. That is the statement "M is a model of my theory T under a given interpretation I" can flip-flop between true and false and back again as you continue to expand your background model of your metatheory (think of e.g. Cohen forcing). So while you may have specified exactly one model, it's getting pretty hard to see just exactly which one it is. First-order logic does not have this phenomenon, which is why we can often get away with not going into too much detail about our metatheory in FOL (and why recursive metatheories built of FOL "all the way down" aren't too problematic). If M is a model of T under I then it will continue to be a model of T under expansion of my background model. So as long as I sketch out the basics of my metatheory (and by implication my background model), I know I'm good. Philosophically this means that in the realm of SOL the only way you can be sure that you've really got "the" standard model and haven't mistakenly grabbed another one is if you can confidently state the truth value of every one of a never-ending stream of theorems which cannot be proved using your metatheory. Indeed statements like "Theorem A is independent of theory T" are very murky and difficult to understand in a second-order setting. For example, CH_2 is definitely not provable using second-order PA, but does that mean we can accept systems with either CH_2 or Not(CH_2)? Well that seems to be false if we take "a single canonical model" at face value, which would imply that only one of the two can be "true," but then how do you decide whether to accept CH_2 or Not(CH_2)? No syntactic argument will suffice since we've lost completeness. That's not to say I think that second-order logic has no value. I think second-order logic, interpreted using first-order semantics, is a valuable language. However, I agree very much with Vaananen's contention that in practice, SOL reduces to multi-sorted FOL. > if second-order logic is used in formalizing or axiomatizing mathematics, the choice of semantics is irrelevant: it cannot meaningfully be asked whether one should use Henkin semantics or full semantics. This question arises only if we formalize second-order logic after we have formalized basic mathematical concepts needed for semantics. A choice between the Henkin second-order logic and the full second-order logic as a primary formalization of mathematics cannot be made; they both come out the same. http://www.math.helsinki.fi/logic/people/jouko.vaananen/VaaSec.pdf http://www.math.helsinki.fi/logic/people/jouko.vaananen/VaaS...