[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

[pron]

> The annoying details of type theory don't get in the way until you get to large sets.

I meant set theory there, not type theory.