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

[pron]

Right, ZFC. Almost all mathematicians accept the axiom of choice. The rest are minor nuances that most students won't even encounter and are only ever investigated by logicians. And even the difference between ZF with or without C only manifests with uncountable sets. This is not the case with type theory. AFAIK, the theories can differ on such questions like whether all subsets of a finite set are finite.

When mathematicians, not logicians, learn logic, it should be made to combine with what they actually do. Type theory is not quite there yet, and is still rather inaccessible and arcane, although that may change.

Turing was interested in making type theory approachable to mathematician, and came up with a gradual path to adoption in his 1944 unpublished manuscript The Reform of Mathematical Notation and Phraseology. He writes:

> It has long been recognised that mathematics and logic are virtually the same and that they may be expected to merge imperceptibly into one another. Actually this merging process has not gone at all far, and mathematics has profited very little from researches in symbolic logic. The chief reasons for this seem to be a lack of liaison between the logician and the mathematician-in-the-street. Symbolic logic is a very alarming mouthful for most mathematicians, and the logicians are not very much interested in making it more palatable. It seems however that symbolic logic has a number of small lessons for the mathematician which may be taught without it being necessary for him to learn very much of symbolic logic.

> In particular it seems that symbolic logic will help the mathematicians to improve their notation and phraseology, which are at present exceedingly unsystematic, and constitute a definite handicap both to the would-be-learner and to the writer who is unable to express ideas because the necessary notation for expressing them is not widely known.

> ... It would not be advisable to let the reform take the form of a cast-iron logical system into which all the mathematics of the future are to be expressed. No democratic mathematical community would stand for such an idea, nor would it be desirable. Instead one must put forward a number of definite small suggestions for improvement, each backed up by good argument and examples. It should be possible for each suggestion to be adopted singly. Under these circumstances one may hope that some of the suggestions will be adopted in one quarter or another, and that the use of all will spread.

In the preface to the manuscript, published in Collected Works of A.M. Turing, Volume 4: Mathematical Logic, 2001, Robin Gandy writes:

> Perhaps the most striking thing about this paper is its modesty. Turing was first and foremost a mathematician. He believed that the chief purpose of mathematical logic and the study of the foundations of mathematics was to help mathematicians to understand what they were doing, and could do. In pursuit of this goal, mathematical logicians must perforce construct and manipulate complex formal systems. But they have a duty to explain to mathematicians, in as non-technical way as possible, what they have accomplished. ... Turing disliked those high priests of logic who sought... to blind the mathematician-in-the-street with arcane formalisms.

It is my impression (and I'm not even a mathematician-in-the-street but a programmer-in-the-street) that type theory hasn't yet emerged out of the "high priest" stage.

[Chinjut]

The difference between ZF with and without C doesn't only emerge with uncountable sets, in any significant sense; even, say, the question of whether every countable set of two-element sets has a choice function depends on Choice.

This is orthogonal to the distinction between type theory-style frameworks and everything-is-a-set ZF-style frameworks, as I was noting before. Whether "all subsets of a finite set are finite" or not can be true or false just as well in ZF-style systems as in type theory systems (taking "finite" to mean "having cardinality equal to a natural number", this is basically just the question of whether we are using classical or intuitionistic logic; you can have classical type theories, and you can have intuitionistic ZF-style theories). As I said, let's not conflate the type theory vs. ZF-style axis with the constructive vs. non-constructive axis.

As for what non-logician mathematicians use in practice, almost everything they do could be done in Zermelo set theory simpliciter (making use only of sets of rank less than omega * 2). I doubt the majority of non-logician mathematicians could even reliably correctly list all the axioms of ZFC. Sure, they've been trained ritualistically to say ZFC is what they're using, but they really aren't using ZFC in particular, any more than any other formal system into which their work could be just as well translated (the formal system of higher-order logic corresponding to Boolean topoi with natural numbers and choice, say).

Frankly, type theory is a lot closer to what "actual" (i.e., non-logician) mathematicians actually do than ZF; actual mathematicians don't spend a lot of time talking or thinking about transfinitely iterated sets of sets of sets…. Actual mathematical practice does come implicitly with types; integers are one type of thing, and functions from reals to natural numbers are another type of thing, and sets of complex numbers paired with Booleans are a third type of thing, and one would never ask whether 7 was an element of 3 or the squaring function on integers was an element of the complex number 3 + 5i, etc.

Framing mathematical ontology in terms of types is not some esoteric practice far removed from the mathematician/programmer in the street. If you've ever written a program in C/C++ or Java, you've worked with types.

Finally, your Turing quotes aren't about type theory in particular, but symbolic logic in general. They apply equally so to ZFC or any other such formal system.

[pron]

> Sure, they've been trained ritualistically to say ZFC is what they're using, but they really aren't using ZFC in particular, any more than any other formal system into which their work could be just as well translated

I agree, but that's not my argument.

> Frankly, type theory is a lot closer to what "actual" (i.e., non-logician) mathematicians actually do than ZF

I've seen this claim made many times, and it's quite iffy. Mathematicians may think of types, but those types are not really much closer to type-theoretical formal types than to formal sets.

> and one would never ask whether 7 was an element of 3 or the squaring function on integers was an element of the complex number 3 + 5i, etc.

This is a misrepresentation of formal set theory in practice. No one investigates those anyway, and in proof assistants based on ZFC they are unprovable. I.e. 3 ∈ 7 has some truth value like any proposition but not one that could be determined in the theory, and it is nonsensical. In other words, 3 ∈ 7 has the same meaning as 1/0 in practical formalizations of set theory (like proof assistants): they are both equal to some value, but that value cannot be determined.

> Framing mathematical ontology in terms of types is not some esoteric practice far removed from the mathematician/programmer in the street.

Right, but there are plenty of annoying details. Even with simple questions such as what 1/0 means: if it's well typed you need to introduce partial functions which are not a familiar or simple concept; if it isn't, you need to introduce dependent types, with their own world of pain. The annoying details of type theory don't get in the way until you get to large sets.

See Leslie Lamport's discussion on the use of types in math[1].

In any event, I think TT should take some more time to mature and become canonized.

> Finally, your Turing quotes aren't about type theory in particular, but symbolic logic in general. They apply equally so to ZFC or any other such formal system.

Yes, but the paper talks about gradually introducing mathematicians to "naive" type theory (Turing wrote a couple of papers about making type theory practical). But my point is about his approach: logicians must make their formal systems approachable. Set theory (at least the part that concerns most ordinary math) is very approachable. Type theory isn't yet.

[1]: Types Are Not Harmless, 1995 research.microsoft.com/en-us/um/people/lamport/tla/types.ps.Z

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