This might be more a MathSE question, but on the other hand, it would involve a peculiar reimagining of the relation between set theory and type theory, so I'll try it out here.

OK, so earlier I thought something like sets/elements:types/tokens. I know the tokenhood relation doesn't figure much (if at all) in what is referred to as type theory proper (at least, I think I gleaned that from at least one or two SEP articles). But anyway, alongside the tokenhood relation, there is an occurrence relation. It is not clear to me that there is a third concept, besides of sets and elements, that appears in set theory, such as could be paired with the occurrence relation, unless we switched things out so that sets/elements:types/occurrences or sets/elements:occurrences/tokens. At any rate, we'd have two set-theoretic descriptors, and three type-theoretic ones.

So this is what I was wondering. On this picture of things, would it be possible to express the set-theoretic relation as a 2-ary case of what is a 3-ary relation in type theory? Then, if we generalize over the numbers at least across the range of n, we would have an endless sequence of forms of such relations. Would general analysis of this sequence constitute a form of category theory? For here categories would be a generalization over sets and types.

Of course, depending on one's opinion about the fundamental status of natural-numbered arithmetic, there might be something jarring about a natural-numbered sequence of something besides those numbers themselves, forming the essence of all mathematics. In other words, if numbers are "under" categories, how yet do they serve as the very index of what it is to be a category (to be an n-ary case of a certain kind of relation)? Perhaps numbers and categories are both fundamental and irreducible to examples of the other.

An even broader objection I can anticipate is that this would pose the question of whether we could generalize over the sequence of relations as a whole itself, so that we could reimagine categories all over again, as variations over such a hypersequence; and so on and on. Then category theory's local definition would never seem to be quite pinned down.

  • Why don't you replace sets with multisets? Then you will have sets/elements/instances : types/tokens/occurrences, symmetry restored. But I do not follow what "if we generalize over the numbers at least across the range of n, we would have an endless sequence of forms of such relations" means. What would be the fourth descriptor, let alone n-th, for either of them?
    – Conifold
    Nov 29 '21 at 8:00
  • quite complex... we can consider W&R's logicism into Principia as a way to formulate the "logical theory or relations", starting from the point of view that mathematics deals not with quantity but with relational structures. Nov 29 '21 at 12:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.