[Kutta]

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.

[pron]

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

[Kutta]

I'm fine with classical reasoning and uncomputability, and I acknowledge the intuition for classical truth (it got popular for a reason). But pretty much all the useful classical math can be performed all the same in type theory without significant change, therefore the presence of "useful math" is not an argument for or against type theory and classical foundations. Rather, the main thing is that type theory is just better for formalizing things, and while type theory can conveniently embed classical reasoning and talk about various levels of constructivity, classical foundations is not convenient for constructive reasoning. Math with justification in ZFC is useful in practice, but ZFC itself is mostly not. I would like to see eventually many or event most things formalized, and for that we need fundamentals for more than justification.

On the more philosophical side, "philosophers should care about computational complexity", certainly, but it's not like one cannot have gradation in philosophical appeal. Also, it definitely helps to have computation at hand if we want to talk about feasible computation.

[pron]

> therefore the presence of "useful math" is not an argument for or against type theory and classical foundations

I wasn't making an argument against type theory (although constructive analysis is quite different from classical analysis) but an argument against a weak argument against classical math. Useful math is very much an argument in favor of a foundation. In fact, it was the winning argument in favor of ZFC, when it was thought that intuitionism would mean radically changing analysis.

> Rather, the main thing is that type theory is just better for formalizing things

In mechanical proof checkers? Then say that type theory is a more convenient small core for a mechanical proof checker. But you're arguing for constructive math, and constructive math is significantly less convenient for proving many things (and constructivists openly acknowledge that).

> ZFC itself is mostly not.

Useful for what? Mathematical foundations are not used when doing math unless you're doing formal math. ZFC seems a lot more useful that type theory when, say, teaching mathematical foundations (which, to reiterate, don't really mean the actual foundations of math).

> I would like to see eventually many or event most things formalized, and for that we need fundamentals for more than justification.

OK, formalizing mathematics is a 100 year old dream and a noble one, but one that may not be shared today by most mathematicians today. Your argument would be clearer and less religious if you said: I want to formalize math mechanically, and currently type theory seems more convenient for that particular task than ZFC.

> but it's not like one cannot have gradation in philosophical appeal

Sure, but I don't understand the aesthetic gradation. Does a mathematical foundation become more appealing to you the more closely it constrains math to the physical? Why? Would a mathematical foundation that doesn't allow expressing speed quantities greater than the speed of light be appealing to you?

I would understand if you said you're an intuitionist, but the intuitionists really did have a problem explaining the effectiveness of classical math (which is simply invalid to them). Classical analysis coincides with constructive analysis on all physically observable propositions and is still easier to work with (at least currently).

> Also, it definitely helps to have computation at hand if we want to talk about feasible computation.

There is absolutely nothing wrong, missing, or inconvenient with how classical math models computation. Type theory or any other constructive math has no advantage there. It certainly doesn't make talking about feasible computation easier.

[Chinjut]

I think it's worth distinguishing "constructive vs. non-constructive" and "ZF style vs. type theory" as different axes, which I think are getting conflated a bit here; you can have type theory style formal systems that embody non-constructive/non-computational principles, and you can have ZF style systems limited only to constructive reasoning (in the sense of Heyting-style intuitionistic logic, say).

Having distinguished these axes, for what it's worth, I don't think ZF-style theories of the cumulative hierarchy of transfinitely iterated sets of sets of sets…, and everything else as encoded into this by hook or by crook, have any advantage over type theory in teaching mathematical foundations, and indeed have some notable drawbacks.

[pron]

I agree, except that when people say "set theory" today, referring to formal set theory, they mean ZF by default, whereas when they say "type theory" it's unclear which type theory they mean. This alone suggests that type theory (or theories, rather) may not be ready for pedagogical use just yet.

[Chinjut]

Not everyone who says "(formal) set theory" means ZF by default. After all, many mean ZFC; probably moreso than mean ZF simpliciter. And some mean ZFC + various large cardinal axioms. Others go the other way, intending only Zermelo set theory. Some others default to meaning IZF or CZF. Some would even push for Aczel's Anti-foundation Axiom as cleaner system instead. Even in a world of sets of sets of sets of sets…, "set theory" does not mean just one particular formal theory.

[nuncanada]

I must the only crazy guy that thinks Boltzmann and Weierstrass got the wrong axiomatization and Real Number Set is an oxymoron? They are completely physically unrealizable.

Every number that is not computable in the the Real Set is also not possible to be written down, don't have an algorithm for it, we can't even talk about or name any of them. All we can talk about is this uncountable part of the Real Set as a Set but never about one of the numbers itself.

[pron]

It's not like this issue hasn't come up, you know. That was at the core of the controversy between Hilbert and Brouwer. But if you think that math must be constructive you must realize that the ramifications are significant and the resulting math is very different and has its own counter-intuitive results. For one, analysis becomes much harder (at least so far) and very different; for example, in intuitionistic math, every function on the reals is continuous. Some counter-intuitive results are that a countable set can have an uncountable subset; in fact, not all subsets of a finite set are even finite. Andrej Bauer wrote a nice, mostly readable introduction to constructive math, which you may find interesting: http://www.ams.org/journals/bull/0000-000-00/S0273-0979-2016...

There are numerous philosophical justifications for non-constructive math, but the pragmatic one is that it is -- as far as we know -- consistent, and coincides with constructive math in all physically realizable instances. Hilbert, for example, said that math has "real propositions" (with physically observable consequences), as well as formalistic propositions, which we can accept as they agree with the real propositions in all instances.

[AnimalMuppet]

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

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]

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