3 ms·
The title "Mathematics in type theory" is like mathematics in real analysis or set theory.
by h8hawk 6y ago
The title "Mathematics in type theory" is like mathematics in real analysis or set theory.
- AnHonestComment 6y agoThe point is that it’s like mathematics in set theory. Type theory is an alternative foundation.
- guerrilla 6y agoIt is like mathematics in set theory, as set theory can be used for a foundation of mathematics; however, it is not like real analysis, because real analysis cannot be used as a foundation for mathematics (without torture.)
- h8hawk 6y agoI think you missed my point. The type theory is mathematics. So saying that math in type theory is nonsense.
- guerrilla 6y agoI'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 agoI 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 agoThey are mathematics: mathematics about mathematics is what metamathematics means.
- lmm 6y agoNo 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.