Let's say we want to come up with a foundational theory for all of mathematics and let's say that it is embedded in first-order logic. Note that the machinery of first-order logic is described with set-theoretical notions, in a meta-theoretical sense.

Why doesn't meta-theoretical use of sets while laying down a foundational theory (intended to avoid sets in an object-theoretical sense) undermine the whole enterprise?

  • Interesting discussion here about set theory vs. category theory as a foundation for mathematics – Hypnosifl Aug 17 '19 at 21:29
  • Well, mathematical foundations don't need to be embedded in FOL. In "From Set Theory to Type Theory", Mike Shulman describes how type theory isn't built on FOL, even though it has FOL: golem.ph.utexas.edu/category/2013/01/… – Alexis Aug 18 '19 at 1:28
  • Keep in mind that in modern times, one of the main applications of formal logic is to be a tool for doing mathematics and computer science, most of the development of formal logic you see is in a form suitable for that application. With the foundational crisis long behind us, there isn't widespread interest in that particular application of formal logic. And given that there are systematic ways to translate between different approaches to the topic, there is even less interest in the specific form in which foundations takes. – user6559 Aug 18 '19 at 7:17
  • @Hurkyl this sounds like something worth elaborating into a full answer. – Aleksandr Aug 18 '19 at 12:08

Your Answer

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

Browse other questions tagged or ask your own question.