1

Do descriptions like those result in paradox or antinomy like "set of all sets" or (nLab seems to say at one point) "category of all categories" do? It seems that the type of types would be a token (or occurrence?) of itself. If it is a token, then it is also a token of the type of tokens. But this seems to make the type of types lesser than the type of tokens. (Maybe there's only a type of types or only a type of tokens; or there should be neither at all!)

Is this (or something like this) a counterpart distortion among types to set/category distortions? Note: I haven't even gotten into the full issue of occurrences vs. tokens, which I don't fully grasp.

I tried Google-searching "type of types" and "is a token of itself" and didn't find the analysis I was wondering about. I don't have an academic subscription to any journal set so I'm not sure where else to look.

EDIT: I did just find some of this analysis in the SEP article on type theory, for "type of types" but not "type of tokens" (or "type of occurrences").

Kristian Berry
  • 9,561
  • 1
  • 12
  • 33
  • 2
    Aristotle argued back in the day that there can be no ["highest genus"](https://plato.stanford.edu/entries/categories/#AriRea), but they do have the highest type/class in programming languages with a hierarchy of classes structure, e.g. in [Smalltalk](https://en.wikipedia.org/wiki/Metaclass#In_Smalltalk-80) there is the Metaclass. – Conifold Mar 04 '21 at 18:53

1 Answers1

1

your first question is closely related to Girard's paradox, which shows that a type of types containing a term Type: Type renders the logic inconsistent. But I think such a result holds only for a certain class of type theories. As @conifold notes, they can be very useful in computation generally, even if not mathematically sound. (but this is true for much of computation anyway).

As for token vs occurence: see my answer here Can something be both a type and a token?.

Lastly, token is not really a term of type theory (haha). That is, mathematical type theories distinguish between types and terms. In philosophy and linguistics, people distinguish between types and tokens. If you work in an area between the two, the context should make it clear which distinction people are referring to.

emesupap
  • 1,959
  • 1
  • 4
  • 12