Type Theory and Principia Mathematica Part IV "Relation Arithmetic" As


type theory is a principle focus of modern computer science,
its origins are in Bertrand Russel's theory of types,
Principia Mathematica is both the origin of and is expressed in the theory of types, and
relational databases are among the highest value, most researched applications of computer science


it seems Russell's "Relation Arithmetic"* (developed in Principia Mathematica Part IV "Relation Arithmetic") would be an active field of study in modern computer science.

In "My Philosophical Development", of Principia Mathematica Part IV "Relation Arithmetic", Bertrand Russell laments:


  "I think relation-arithmetic important, not only as an interesting
  generalization, but because it supplies a symbolic technique required
  for dealing with structure. It has seemed to me that those who are not
  familiar with mathematical logic find great difficulty in
  understanding what is meant by 'structure', and, owing to this
  difficulty, are apt to go astray in attempting to understand the
  empirical world[emphasis JAB]. For this reason, if for no other, I am sorry that the
  theory of relation-arithmetic has been largely unnoticed."


Is Russell's theory of relation-arithmetic still largely unnoticed even in modern computer science based on type theory, despite the critical role computers play in bringing mathematical understanding of the empirical world into practical use?  If so, why?

*A good, informal, introduction to relation-arithmetic is in Introduction to Mathematical Philosophy, by Bertrand Russell.  One must first understand Russell's abstract definition of "number", drawn from Frege (Chapter II "DEFINITION OF NUMBER").  Then one can proceed to Chapter VI "SIMILARITY OF RELATIONS" where he defines relation-arithmetic.

Briefly, there are no "sets" in the sense we think of "set theory" -- there are only "relations" which may be "similar" to one another.  All relations that are "similar" to one another comprise a "relation number".  Similarity between two relations, P and Q, obtains if there is a one-to-one correspondence between the relata of P and the relata of Q such that if a relationship holds in P, the relationship also holds in Q between its corresponding relata.  One can even think of ordinary numbers as relation numbers if one restricts the relations to one place relations (monadic/unary/property/etc.).  I emphasize this because although Russell uses the word "class similarity" rather than "relation similarity" in Chapter II, it is apparent that he considers "class" to be a degenerate case of "relation" when one carefully reads Chapter IV.  Because of this, and the fact that type theory is considered an alternate foundation for mathematics used in computer science, it may be incorrect to dismiss relation-arithmetic as a degenerate case of category theory or some other more complex mathematical structure in which it may be encoded or modeled.  Such modeling or encoding should be the other way around.

"Relation numbers", thus defined, are then defined to have the ordinary arithmetic operators, addition, multiplication and even exponentiation.
relational databases are among the highest value, most researched applications of computer science
  


James, what do relational databases have to do with the question? And why have you tagged this q with 'relational-algebra'? It seems to me entirely gratuitous.

Just because databases are 'relational' does not mean they have much to do with whatever Russell meant by 'relation-arithmetic'.

Relational database theory sticks to simple set theory and FOPL. Precisely because it wants to avoid getting into higher-order complications (and type theory).

Similarly just because historically Russell's theory of types kicked off an area of research, does not mean that everything these days to do with type theory must therefore derive from Russell, or that his later musings would necessarily help.


  Is Russell's theory of relation-arithmetic still largely unnoticed even in modern computer science based on type theory, despite the critical role computers play in bringing mathematical understanding of the empirical world into practical use? If so, why?


I'd say yes, entirely unnoticed.

Again what relevance does the "critical role computers play" have wrt Russell?

On looking at a few of the standard early works in programming language type theory, I see no citations of Russell: Landin 1965 on the semantics for ALGOL; Strachey 1967; Reynolds 1983.

The Reynolds paper has the word "relations" in the abstract. And cites a paper Morris 1973 'Types are not Sets'. And mentions [Dana] "Scott's discovery of how to construct sufficiently rich universes without encountering Russell's paradox".

Modern type theory derives mostly from typing models for Lambda Calculus; of which Russell had no inkling. That could be why.

BTW your opening link to the answer on type theory, which mentions "Russell's paradox occasionally shows up" then points to some results in Haskell I think is again drawing a very long bow. Also those results back in 2010 are for some early developments of then-new type-level features. I'd classify them as bugs. They rely essentially on Impredicativity about which the compiler's user guide says "GHC has extremely flaky support for impredicative polymorphism, ..."; indeed I think the feature is to be blocked as a 'very hard problem to get right'.