4 ms·

Second-order logic is generally avoided in discussion of mathematical foundations because it is not very "foundational"; it is too vague or "mysterious" to serv

by pron 6y ago

Second-order logic is generally avoided in discussion of mathematical foundations because it is not very "foundational"; it is too vague or "mysterious" to serve as a comfortable foundation. Unlike FOL, it itself is incomplete. In a formal set theory, like ZFC, we postulate the existence of the set of natural numbers. This is something most logicians are comfortable with as being "mathematically foundational" ("God made the natural numbers; all else is the work of man"). Then, to describe the set of sets of natural numbers we use the powerset axiom that defines what exactly we mean by "all sets of natural numbers." Then, Löwenheim–Skolem appears and says that there are models of this set theory where the number of sets that satisfy this definition is countable (not inside the logic, but looking from the outside), to which we say: well, so be it. The reason this happens is because there is a fundamental limitation to the power of describing things using finite strings of symbols. Second-order can just say, no, when I say "all subsets" I mean absolutely all. But can we precisely formalise, i.e. write down in symbols, what we mean by "all" using some basic, "simple" foundation? The answer is no. Second-order logic just vaguely gestures toward "all" and says, "by all we mean all". It circumvents the limitations of formalisation -- i.e. describing things in finite sentences -- by alluding to non-describable things. Most logicians feel this isn't very foundational to rely on allusions to things that aren't themselves reducible to axioms in a basic foundation. Even when higher-order logics are used in formal mathematics, like various set theories or Isabelle's HOL, they are (at best) picked to be as powerful as (multi-sorted) FOL rather than "actual" SOL.

pdonis 6y ago
> In a formal set theory, like ZFC, we postulate the existence of the set of natural numbers. But if your theory is a first-order theory, you cannot pin down "the set of natural numbers" to the one you and everyone else is actually thinking of; no matter what set of axioms you use to define "the set of natural numbers" (the Peano axioms, etc.), there will be semantic models other than the set of natural numbers you are thinking of that satisfy those axioms. The only way to precisely pin down "the set of natural numbers" to one semantic model--the one you actually want--is to use second-order logic. So it seems to me that there is a genuine tradeoff here. If you want enough expressive power to be able to precisely pin down what semantic model your theory is talking about, you need to accept that your theory will be making statements that are non-constructive--you can have an axiom that says every set has a power set, but you can't construct that power set in the general case. If you want your theory to be constructive, so that for every set that your theory says exists, you can see how to construct it explicitly, you need to accept that your theory will have multiple semantic models and only one of them is the one you want, and your theory can't pin it down for you.
- pron 6y ago
  It's not about being constructive. ZFC easily allows defining sets non-constructively. It's about accepting a theory whose meaning refers to objects that are not generally viewed as sufficiently basic. There seems to be a limitation on precisely describing uncountable infinities using finite strings of characters from a finite alphabet.
  - pdonis 6y ago
    > It's not about being constructive I agree that "constructive" was not a good term. This... > It's about accepting a theory whose meaning refers to objects that are not generally viewed as sufficiently basic. ...is fine as a better phrasing for what I was thinking of. My point is that there is a tradeoff between the property "the theory is built entirely from objects that are sufficiently basic" and the ability to precisely pin down a single semantic model; having either one means giving up the other.
    - dwohnitmok 6y ago
      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.
      - 6y ago

by pron 6y ago

pdonis 6y ago

> In a formal set theory, like ZFC, we postulate the existence of the set of natural numbers. But if your theory is a first-order theory, you cannot pin down "the set of natural numbers" to the one you and everyone else is actually thinking of; no matter what set of axioms you use to define "the set of natural numbers" (the Peano axioms, etc.), there will be semantic models other than the set of natural numbers you are thinking of that satisfy those axioms. The only way to precisely pin down "the set of natural numbers" to one semantic model--the one you actually want--is to use second-order logic. So it seems to me that there is a genuine tradeoff here. If you want enough expressive power to be able to precisely pin down what semantic model your theory is talking about, you need to accept that your theory will be making statements that are non-constructive--you can have an axiom that says every set has a power set, but you can't construct that power set in the general case. If you want your theory to be constructive, so that for every set that your theory says exists, you can see how to construct it explicitly, you need to accept that your theory will have multiple semantic models and only one of them is the one you want, and your theory can't pin it down for you.

pron 6y ago
It's not about being constructive. ZFC easily allows defining sets non-constructively. It's about accepting a theory whose meaning refers to objects that are not generally viewed as sufficiently basic. There seems to be a limitation on precisely describing uncountable infinities using finite strings of characters from a finite alphabet.
- pdonis 6y ago
  > It's not about being constructive I agree that "constructive" was not a good term. This... > It's about accepting a theory whose meaning refers to objects that are not generally viewed as sufficiently basic. ...is fine as a better phrasing for what I was thinking of. My point is that there is a tradeoff between the property "the theory is built entirely from objects that are sufficiently basic" and the ability to precisely pin down a single semantic model; having either one means giving up the other.
  - dwohnitmok 6y ago
    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.
    - 6y ago