Comment by deepsun

8 hours ago

There is, or rather are, fully recognized axiomatic foundations. You are free to choose one you like. Of the most popular ones is ZFC or ZF, but there are others (some lead to the same results some not). The main criteria for popularity is how useful it is. You can even make your own axiomatic where 2+2=5, but it would be useless.

You probably heard about Goedel Incompleteness -- the proof that the the axiomatic itself cannot be proven, like using ZFC to prove ZFC, but that's another topic.

It would be fun to play with this Anthropic/Lean formalization under different axiomatics.

22 comments

deepsun

Reply
SP3269  7 hours ago

Interestingly, in his ICM 2026 lecture, Terence Tao specifically mentioned that Lean is not based on ZFC.

andriy_koval  8 hours ago

> Goedel Incompleteness -- the proof that the the axiomatic itself cannot be proven, like using ZFC to prove ZFC, but that's another topic.

Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems.

  • drdeca  5 hours ago

    ZFC has greater consistency strength than PA.

    If we take ZFC (or some other set theory) as our meta theory, we can easily see that the axiom of infinity (of ZFC) gives a set of natural numbers (using the von Neumann encoding), which, when equipped with the successor function, is a model of the natural numbers.

    • andriy_koval  4 hours ago

      zfc doesn't have functions, so you are building something new on top of it.

      Also, I am not sure successor function is enough for PA.