[igravious]

to justify my claim with an excerpt from the article:

““ What is type theory

    “Every propositional function φ(x)—so it is contended—has, in addition to its range of truth, a range of significance, i.e. a range within which x must lie if φ(x) is to be a proposition at all, whether true or false. This is the first point in the theory of types; the second point is that ranges of significance form types, i.e. if x belongs to the range of significance of φ(x), then there is a class of objects, the type of x, all of which must also belong to the range of significance of φ(x)” — Bertrand Russell - Principles of Mathematics

In the last section, we almost fell in the trap of explaining types as something that are “like sets, but… “ (e.g. they are like sets, but a term can only be a member of one type). However, while it may be technically true, any such explanation would not be at all appropriate, as, while types started as alternative to sets, they actually ended up being quite different. So, thinking in terms of sets won’t get you far. Indeed, if we take the proverbial set theorist from the previous section, and ask them about types, their truthful response would have to be:

    “Have you seen a set? Well, it has nothing to do with it.” [<=== important bit] 

So let’s see how we define a type theory in its own right. ””

[seanhunter]

The modern formulation of functions as sets doesn’t require type theory but is entirely congruent with Russell’s definition, just much less cumbersome. In this view, φ is a relation on the set (D X C) where D and C are the domain and codomain of the function (which he calls the “range of significance of x” and the “range of significance of φ(x)” respectively). So since he’s talking about propositional functions, here C is the set {true, false} and D is all the things that are like whatever x is ie the set {x’: x’ is of the same type as x}.

Now a relation is just a particular type of predicate (ie it too is a set) so here we have x ~ y if φ(x) = y for all (x,y) in (D X C).

Notice here both the propositional function and the type are sets.

[mrkeen]

Oof. If sets and types aren't the same, then sets and barbers are definitely not the same!