Modern Mathematics is very much influenced by the success of calculus since Newton

That was true in nineteenth century, much less so in twentieth and now. If we are talking about stuff everybody learns in school, then I think the essence of mathematics is much better represented by geometry than calculus.

Why do you prefer set theory?

Of course the choice of foundation is mostly subjective, so I can’t make a good rational argument that set theory is better that type theory for expressing mathematics. This is a matter of training and habit. For most mathematicians it is more natural to express mathematics in set theory because this is how they have been trained (indoctrinated?).

I am a fan of strong typing in programming languages. It is really a cheaper substitute for formal verification – it allows to assert certain properties of software you are writing and then those assertions are checked by the compiler. In this context we can say that types “protect you from writing nonsense” or “keep your story straight”. But in the context of (formalized) mathematics, where you have the real thing (every assertion has a proof), types don’t serve any purpose and only get in the way. See Harisson’s paper on Euclidean spaces for an example of hoops one has to jump to express a very simple concept of $latex R^n$ if the type system is not good enough, the issue about which he says “Of course, no problem arises in systems based on traditional set theory (such as Mizar)”.

]]>Re your first comment: Modern Mathematics is very much influenced by the success of calculus since Newton and only very little by ideas from Computer Science. That’s why I used the, admittedly, provocative phrase “Mathematics is about numbers”.

Re your 2nd. Obviously you have a point: we can use the type/set terminology to indicate the difference between a predicative hierarchy (ala Russell) and the restriction of comprehension (ala Zermelo). However, in Type Theory many people use the term Set to refer to small types, e.g. Coq uses the term Set to refer to Type(0) – the first universe.

Why do you prefer set theory? If you are interested in functional programming this seems slightly incoherent too me.

]]>Thank you for your deep insights…

Well, I shouldn’t be commenting just because I am annoyed, without anything interesting to say.

The first reason I was annoyed was the idea that “mathematics has to do with numbers”. You can look at the comments to this blog post to understand why.

The second reason was the suggestion to call the types “sets”. (Zermelo-Fraenkel) Set theory and type theory are two alternative (I would say competing) foundations for mathematics. They resolve the Russel paradox differently. They have different axioms and are just different. Types and sets should not be confused. I prefer set theory as a foundation for mathematics, but of course this is a matter of taste.

]]>expressions {x | P(x) }, where P(x) is a formula with x free.

Set theorists are reasonably well-behaved about observing this terminological distinction, and it causes little problem.

“Type theory” is by comparision a terminological pig-sty. To my mind,

we should use the word “set” for an object of type Set, and “type” like

the set-theorists use “class”. We should use words like “small”, “large”,

“hyper-large” and so on to distinguish sets that have names in universes

inside Set. But even I don’t: it depends on who I am speaking to. There

are things that just fall off the tongue, like “W-type” that are just beyond

repair.

A number of people have struggled (a bit desperately) to find some terminology

that fits both what people actually say, and reality. There has been

“type/category” for “set/type” (in the Bibliopolis book), and I think

“type/kind” by Luo. And the “set/type” distinction has been more or less

scotched by the rise of constructive set theory, taking over the “S”-word

for something like its use in conventional set-theory.

We are all doomed. DOOMED!

Hank

]]>Hence I think that the terms sets and types have no clearly identifiable meanings and overlapping interpretations. I treat them basically as synonyms.

Thorsten ]]>

Mathematics has to do with numbers, while Computer Science is more concerned with types (let’s call them sets)

No. Mathematice has to to with sets (let’s call them sets), while Computer Science is more concerned with types (let’s call them types).

]]>