There seem to be, broadly speaking, three1 distinct foundations of mathematics: set, type and category theory (the latter as per Lawvere), in which it should be possible to formalize all mathematics except perhaps the theories themselves. For example, I've got a (rather vague) impression that you can formalize all set theory in category theory and vice versa, while you cannot formalize higher inductive types (a foundational tenet of HoTT) in set theory (and I'm not confining type-theoretical foundations of maths to HoTT, it's just an example). So my question is: for all the (three?) foundations, what are their features that cannot be formalized in others? (If you could make a very long list, consider making an overview instead)

EDIT: I understand that the question is difficult, owing to the facts that (1) very few people would be sufficiently knowledgeable to answer it, (2) it's very difficult to prove that something's impossible (and negative existential proofs can be only classical, which undermines their usefulness), and (3) a conjecture is likely to incite an arms race between the theories. Nevertheless, it would be interesting to know what others think

1 @user170039 also mentioned mereology


closed as off-topic by Andrés E. Caicedo, Shailesh, Xander Henderson, Namaste, Taroccoesbrocco Jun 25 '18 at 8:13

This question appears to be off-topic. The users who voted to close gave this specific reason:

  • "This question is missing context or other details: Please improve the question by providing additional context, which ideally includes your thoughts on the problem and any attempts you have made to solve it. This information helps others identify where you have difficulties and helps them write answers appropriate to your experience level." – Andrés E. Caicedo, Shailesh, Namaste
If this question can be reworded to fit the rules in the help center, please edit the question.

  • 1
    $\begingroup$ If you read this MO question, you'd find reasons why mereology isn't really a suitable foundation for mathematics. $\endgroup$ – Asaf Karagila Jun 24 '18 at 20:31
  • 2
    $\begingroup$ Who is claiming that higher inductive types can't be formalized in set theory? $\endgroup$ – Noah Schweber Jun 24 '18 at 20:32
  • $\begingroup$ And of course you can formalize HTT in set theory. You just need to add some reasonable axioms to formalize universes. $\endgroup$ – Asaf Karagila Jun 24 '18 at 20:32
  • $\begingroup$ @Noah: The OP, duh. :) $\endgroup$ – Asaf Karagila Jun 24 '18 at 20:35
  • 3
    $\begingroup$ Just because something is impossible to capture directly doesn't mean it is impossible to capture. You can't take a photo of the wind, but you can disperse smoke into the wind, and take a photo of the smoke. $\endgroup$ – Asaf Karagila Jun 24 '18 at 20:53