| > 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 |
I meant set theory there, not type theory.