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