*Sorry if this is off-topic*.

It was my attempt to take a top-down approach to mathematics.

Being an inexperienced undergraduate (so please take my writing here lightly), I've been presented with ZFC as a foundational system. However, other set theories exist (e.g. NBG), the axiom of choice is famously "controversial", and then there's other approaches entirely, like type theory (e.g. HoTT) and category theory.

*Alright*, but these seem to have some structure in common... enter universal logic, for which I found Meseguer's paper particularly enlightening. For a brief moment I thought I had reached my goal (despite the fact that the theory about logics was itself already quite mathematically sophisticated).

But then I discovered that, to describe different logics, one needs (or desires?) a logical framework to operate in. Pfenning's paper gives a lovely introduction to this topic, but also mentions that there are a multitude of logical frameworks, e.g. ELF or Martin-Löf's Framework, so I'm still not where I want to be.

Then, finally, I came across a paper entitled "A Framework for Defining Logical Frameworks". At this point I thought to myself that perhaps my approach thus far is misguided, given that the more effort I make, the less clear things seem to become.

And hence, my question: *Where does it all begin?*

Or, should this be unanswerable, is there some sort of guide through this flurry of terminology and meta-metamathematical research? It seems authors have such a clear grasp on the confines of each topic, yet somehow I cannot satisfy my simple desire to find a point at which to start. *What would Bourbaki do*, if they were to start writing *today* instead of 80-something years ago?

7more comments