4 ms·

I think you missed my point. The type theory is mathematics. So saying that math in type theory is nonsense.

• guerrilla 6y ago
  I'm sorry but you misunderstand the situation. Set theory, type theory and category theory can be used for metamathematics [1] whereas real analysis and number theory cannot. They are foundational theories whereas real analysis and number theory are not. The reason for the difference has to do with the expressiveness of the formal languages and how they themselves can be expressed without a prior language other than formal logic itself. [1]. https://en.wikipedia.org/wiki/Metamathematics https://en.wikipedia.org/wiki/Metamathematics [2]. https://en.wikipedia.org/wiki/Foundations_of_mathematics https://en.wikipedia.org/wiki/Foundations_of_mathematics
  • h8hawk 6y ago
    I know they are foundations of mathematics. They are elements of mathematical logic. No disagreement on this. But how they are not mathematics? They are part of mathematical logic and mathematical logic or logic in general is branch of mathematics. Do you want to say they are somehow separated from math?
    • guerrilla 6y ago
      They are mathematics: mathematics about mathematics is what metamathematics means.
• lmm 6y ago
  No more nonsense than studying English in English. It is true that type theory is mathematics, but the relevant fact is that it (unlike many fields of mathematics) is suitable for studying mathematics with.