5 ms·

Precisely. Any attempts of even discussion about Higher Order theories on that list ends up with Harvey stating something that can be translated to those withou

Precisely. Any attempts of even discussion about Higher Order theories on that list ends up with Harvey stating something that can be translated to those without the technical expertise as "Every higher order theory is a first order theory in disguise". Which is true but besides the point. Just look at Peano's axiomatization of the Natural Numbers and perceive how intuitively bad it is at abstracting what Natural Numbers are. He constructs an "ugly" object that is isomorphic to Natural Numbers, but doesn't correspond to what Mathematicians intuitively believe the Natural Numbers to be. With a Second Order theory you can just axiomatize the Natural Number in a pretty straightforward way that correspond to Mathematician's intuition about the Set...

Pete_D 10y ago
At the risk of asking a naïve question, why do you think the Peano axioms are ugly? As a mostly-lay mathematician I always thought they were quite elegant.
- Kutta 10y ago
  My perspective is that classical axiomatic theories have a far weaker philosophical grounding than constructive type theories. In type theory every definable natural number is a program which evaluates to a concrete finite numeral. You can't get more grounded than that. Of course, there is still a large variety of standard and nonstandard models of type theory as well, but the computational interpretation already corresponds very closely to intuitions about intended (standard) models. In contrast, the lack of clear computational meaning in classical theories makes it necessary find philosophical justifications, which in turn usually refer to other theories without clear computational meaning. Of course, we can compile classical proofs to programs as well through a variety of transformations, but they tend to be sort of unsatisfying, for example we may get functions with empty domains that we can't actually call, instead of programs evaluating to numerals. So, Peano arithmetic is just too loose and fuzzy for my taste. It's full of things which aren't numbers, rather statements referring to things which have properties which we think numbers should have. And then we can choose between sticking to first-order logic and leaving non-standard models in, or switching to second-order induction which lets us prove more statements at the cost of completeness and leaning more on ambient set theory. Simpson seems to be critical of second-order logic because it's set theory in disguise; but to me that kind of dispute is moot because I find any sort of classical logic unsuitable for mathematical foundations.
  - AnimalMuppet 10y ago
    > So, Peano arithmetic is just too loose and fuzzy for my taste. It's full of things which aren't numbers... OK. > In type theory every definable natural number is a program which evaluates to a concrete finite numeral. To me, that sounds like type theory is also full of things that are not numbers, namely computations. ("Evaluates to a natural number" != "is a number".)
    - Kutta 10y ago
      Evaluation is always implicitly used in any sort of mathematical formalism. "2 + 2" is a program which evaluates to "4". Type theory just makes the computation arising from substituting definitions rigorous. Not letting "2 + 2" be equal to "4" by definition would be weird and inconvenient.
      - AnimalMuppet 10y ago
        I get that evaluation is always implicit (or at least implicitly assumed to happen). My quarrel is with "evaluation == program == computation", and even more with the reverse: "a number == computation that would produce the number, therefore number == computation".
  - pron 10y ago
    You are making a philosophical choice that was heavily debated in the early 20th century, namely, you contend that a mathematical foundation is truly foundational (perhaps even unique), and that math is built on top of one. Another alternative (favored by Turing[1]) is that any mathematical foundation is just like any other calculus, only one that deals with the lower-levels of mathematics. Also, by picking computation as the "true" foundation, you are being a bit arbitrary. On the one hand, you can get more grounded. Computability was justified on physical arguments, and Turing and others recognized that computability is only a rough approximation of feasibility, which was given a more precise treatment much later. So if you want to base the foundations of math on the physical -- which is what you're doing if you're basing them on Turing computability -- then you can go a lot further down towards "grounded". On the other hand, there is really no reason to limit math at the computable. Brouwer thought there was, but Turing didn't. If non-constructive math yields results that are useful, compatible with constructive math and is easier to work with in some cases, what justification is there to reject it other than by taking a view that is both fundamentalist (in the sense I described) and somewhat arbitrary? After all, constructive math is a very different math, and if classical math rests on shaky foundations, how is it so useful in practice, and how come it agrees with constructive math on everything that is physically observable? [1]: https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf
- nuncanada 10y ago
  A simple answer would be: the Natural Numbers can be axiomatized infinitely many different isomorphic ways in First Order Theories. Which one is the "right" one? None and according to FOM wisdom you shouldn't care. In Higher Order Theories there is a very straightforward and natural way to define the Natural Numbers. Could you create other isomorphic axiomatizions? Yes but they certainly wouldn't be as pleasant and straightforward...

Pete_D 10y ago

At the risk of asking a naïve question, why do you think the Peano axioms are ugly? As a mostly-lay mathematician I always thought they were quite elegant.

Kutta 10y ago
My perspective is that classical axiomatic theories have a far weaker philosophical grounding than constructive type theories. In type theory every definable natural number is a program which evaluates to a concrete finite numeral. You can't get more grounded than that. Of course, there is still a large variety of standard and nonstandard models of type theory as well, but the computational interpretation already corresponds very closely to intuitions about intended (standard) models. In contrast, the lack of clear computational meaning in classical theories makes it necessary find philosophical justifications, which in turn usually refer to other theories without clear computational meaning. Of course, we can compile classical proofs to programs as well through a variety of transformations, but they tend to be sort of unsatisfying, for example we may get functions with empty domains that we can't actually call, instead of programs evaluating to numerals. So, Peano arithmetic is just too loose and fuzzy for my taste. It's full of things which aren't numbers, rather statements referring to things which have properties which we think numbers should have. And then we can choose between sticking to first-order logic and leaving non-standard models in, or switching to second-order induction which lets us prove more statements at the cost of completeness and leaning more on ambient set theory. Simpson seems to be critical of second-order logic because it's set theory in disguise; but to me that kind of dispute is moot because I find any sort of classical logic unsuitable for mathematical foundations.
- AnimalMuppet 10y ago
  > So, Peano arithmetic is just too loose and fuzzy for my taste. It's full of things which aren't numbers... OK. > In type theory every definable natural number is a program which evaluates to a concrete finite numeral. To me, that sounds like type theory is also full of things that are not numbers, namely computations. ("Evaluates to a natural number" != "is a number".)
  - Kutta 10y ago
    Evaluation is always implicitly used in any sort of mathematical formalism. "2 + 2" is a program which evaluates to "4". Type theory just makes the computation arising from substituting definitions rigorous. Not letting "2 + 2" be equal to "4" by definition would be weird and inconvenient.
    - AnimalMuppet 10y ago
      I get that evaluation is always implicit (or at least implicitly assumed to happen). My quarrel is with "evaluation == program == computation", and even more with the reverse: "a number == computation that would produce the number, therefore number == computation".
- pron 10y ago
  You are making a philosophical choice that was heavily debated in the early 20th century, namely, you contend that a mathematical foundation is truly foundational (perhaps even unique), and that math is built on top of one. Another alternative (favored by Turing[1]) is that any mathematical foundation is just like any other calculus, only one that deals with the lower-levels of mathematics. Also, by picking computation as the "true" foundation, you are being a bit arbitrary. On the one hand, you can get more grounded. Computability was justified on physical arguments, and Turing and others recognized that computability is only a rough approximation of feasibility, which was given a more precise treatment much later. So if you want to base the foundations of math on the physical -- which is what you're doing if you're basing them on Turing computability -- then you can go a lot further down towards "grounded". On the other hand, there is really no reason to limit math at the computable. Brouwer thought there was, but Turing didn't. If non-constructive math yields results that are useful, compatible with constructive math and is easier to work with in some cases, what justification is there to reject it other than by taking a view that is both fundamentalist (in the sense I described) and somewhat arbitrary? After all, constructive math is a very different math, and if classical math rests on shaky foundations, how is it so useful in practice, and how come it agrees with constructive math on everything that is physically observable? [1]: https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf
nuncanada 10y ago
A simple answer would be: the Natural Numbers can be axiomatized infinitely many different isomorphic ways in First Order Theories. Which one is the "right" one? None and according to FOM wisdom you shouldn't care. In Higher Order Theories there is a very straightforward and natural way to define the Natural Numbers. Could you create other isomorphic axiomatizions? Yes but they certainly wouldn't be as pleasant and straightforward...