[jhuni]

> Type theory and accompanying first-order logic is the foundation upon which mathematics is built.

Since when? Mathematics was originally founded on the study of the natural numbers. The mathematics I find most valuable (eunmerative combinatorics) still uses the natural numbers as its foundation and not type theory.

[maaku]

Number theory/abstract algebra, which is the study of natural numbers among other things, is a form of set theory. And set theory is what mathematics calls type theory.

[jhuni]

> Number theory/abstract algebra, which is the study of natural numbers among other things, is a form of set theory.

Let S be the set {a,b} and let T be the set {c,d}. There are two bijections S -> T between these two sets {(a,c),(b,d)} and {(a,d), (b,c)}. These two sets are isomorphic to one another because they have the same cardinality.

The isomorphism classes of sets are cardinalities which are themselves the natural numbers 0,1,2,3,... and infinity. In combinatorics we can just focus on the study of these isomorphism classes rather then sets themselves.

We can enumerate binary relations: ([],[0],[1],[[0 0],[0 0]],[[0 0],[0 1]],[[0 0],[1 0]],[[0 0],[1 1]],[[0 1],[0 0]],[[0 1],[0 1]],[[0 1],[1 0]],[[0 1],[1 1]]). Logical disjunction [[0,1],[1 1]] is equal to 10 in this enumeration.

Using the enumeration of binary relations the entire field of study of graph theory can be described in terms of natural numbers without any need for sets. As a result, graph theory is considered to be a branch of combinatorics. We only need to have sets mathematically when dealing with cardinalities like aleph one that emerge from uncountable sets.

Since analytic number theory deals with the uncountable set of real numbers and abstract algebra deals with operations on sets including the real numbers, these two fields are indeed founded on set theory. Algebraic combinatorics and combinatorial number theory are the branches of these two fields that focus on countable sets.

> And set theory is what mathematics calls type theory.

No it isn't. Just look up differences of type theory from set theory on wikipedia [1]. You almost never hear the word "type" spoken in math courses. According to John Shutt "I took some tolerably advanced math courses in college and graduate school. One thing I never encountered in any of those courses, nor that-I-recall even in the THUG talks, was a type. Sets aplenty, but not types" [2].

[1] Type theory differences from set theory http://en.wikipedia.org/wiki/Type_theory#Difference_from_set...

[2] Where do types come from http://fexpr.blogspot.com/2011/11/where-do-types-come-from.h...

[maaku]

> No it isn't ... You almost never hear the word "type" spoken in math courses.

You misread me. What I said was that "set theory" is the general mathematical framework exactly equal to what we computer scientists call "type theory". We have completely different ontologies for what are essentially the same thing (the differences listed on Wikipedia are superficial/conventional and IMHO of no relevance here or in the article).

Mathematicians deal with sets, countable or otherwise, algebraic manipulations of them, bijective mappings, etc. Computer scientists operate on domains (types), their operators, functions, etc. These are different terminology for the exact same thing.

[jhuni]

> You misread me. What I said was that "set theory" is the general mathematical framework exactly equal to what we computer scientists call "type theory".

That makes more sense. I am coming from a mathematical background and not a computer science background myself.

> Mathematicians deal with sets, countable or otherwise, algebraic manipulations of them, bijective mappings, etc.

That is true. As a combinatorist I am one of those people who mainly focuses on countable sets. The isomorphism classes of sets (the counting numbers) are at the foundation of everything I do in combinatorics but other areas of mathematics (e.g topology) have very different approaches.