It is well known that the theory of types, first introduced by Bertrand Russell in 1903 and developed with Whitehead in their Principia Mathematica (1910), was a way to deal with paradoxes in set theory. Type theory was later developed by Church, Per Martin-Löf and many others.

In type theory, every mathematical object belongs to a type. One could link this with the fact that in physics every quantity has a unit. Knowing that units were introduced in physics certainly well before types found their way explicitly in logic, did units in physics play any role in the introduction of types in logic and the foundations of mathematics?

  • 1
    $\begingroup$ Not really. Dimensional quantities are more analogous to sorts in many-sorted logic than to types that fall into a hierarchy absent with different dimensionalities. $\endgroup$
    – Conifold
    Nov 9 '20 at 19:24
  • $\begingroup$ I agree, but on the other hand you can't build new sorts from previous ones. In many-sorted logic one seems to start with a fixed set of sorts, whereas in physics you can build new units from previous ones and same thing in type theory where one can build new types from previous ones (aka dependent types), at least if one is not restricted to a so-called simple type theory. $\endgroup$ Nov 9 '20 at 21:17

And even before units were introduced in physics, people knew, for example, not to add oranges to say, apples. At least this is what I was taught in primary school, and I imagine that this goes back a long way.

Unless some evidence turns up showing that Russell or Whitehead were directly influenced by the notion of dimension in physics, I'd say this is just as likely to be an independent rediscovery - as so often happens in physics and mathematics, one of the most notorious example being the independent discovery of calculus by Newton and Liebniz.

In type theory every mathematical object belongs to a type

Proofs, as mathematical objects, also denote types. However, this doesn't obtain in physics. In physics, we don't tend to have proofs, rather we have arguments. This is something that the more mathematically orientated physicists have a hard time understanding...

  • $\begingroup$ In the Brouwer-Heyting-Kolmogorov paradigm of "propositions as types", proofs are inhabitants of types. The physics equivalent would be some physical quantities having (or realizing so to speak) some given dimension. $\endgroup$ Nov 13 '20 at 17:03

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.