5 ms·

Not just lean, but math foundation itself, I am not strong expert, but my understanding is that there is no fully recognized axiomatic foundation for modern mat

• ajs1998 1mo ago
  ZFC is probably the biggest foundation, and only Choice is apparently controversial. The results aren't that weird, they're just different and occasionally more useful than using !Choice.
  • andriy_koval 1mo ago
    do we know if claude's formalization is built on top of zfc and not zfc+extra? zfc itself is not sufficient, you need some layers of extra concepts formalization to fit specific problem domain(e.g. zfc doesn't define even basic arithmetics), which also could have potential issues.
    • drdeca 1mo ago
      Within a given inference system, one can define concepts. This doesn’t add any axioms. It is, in essence, just a way to abbreviate things.
      • andriy_koval 1mo ago
        ok, you now added some unknown inference system in addition to zfc
        • drdeca 1mo ago
          No, it is the same inference system. They are just abbreviations.
          • andriy_koval 1mo ago
            and what is that system?
            • drdeca 1mo ago
              ZFC
              • andriy_koval 1mo ago
                zfc is a bunch of axioms and not inference system. It is commonly assumed that it is built on top of some unspecified first order logic which commonly assumed to include bunch of inference rules. There is no ground truth in my understanding where this all is formally defined.
                • drdeca 1mo ago
                  If you want to use “ZFC” to refer to the axioms without any rules of inference, I guess you can do that, but when someone refers to “ZFC” when they are filling a slot that needs a (axioms + rules of inference), the obvious interpretation is that they are referring to the usual system of ZFC.
                  • andriy_koval 1mo ago
                    > when someone refers to “ZFC” when they are filling a slot that needs a (axioms + rules of inference), the obvious interpretation is that they are referring to the usual system of ZFC. its bro-math. In formal math you need to be specific what inference system you use. There are many of them. Then you need to have formal proof that in that system you can derive concept of function and then think about question if it won't make paradoxes and contradictions with ZFC.
    • Smaug123 1mo ago
      Claude’s formalisation, being in Lean, is based on the calculus of inductive constructions, not ZFC. In Lean 3, per Carneiro, any theorem of Lean 3’s theory can be proved in ZFC plus some finite number of inaccessible cardinals (and, IIRC, vice versa). The precise strength of Lean 4 is not quite clear yet, I think (I guess this is partly what Lean4Lean is hoping to address).
  • lanstin 1mo ago
    Reply to sibling - lean4 doesn't rest on ZF or ZFC. https://lean-lang.org/theorem_proving_in_lean4/Axioms-and-Computation/ https://lean-lang.org/theorem_proving_in_lean4/Axioms-and-Co... However I believe an equivalence of power has been shown between the two.
    • mietek 1mo ago
      Roughly, yes. See B. Werner (1997) “Sets in types, types in sets”.
• deepsun 1mo 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.
  • andriy_koval 1mo 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.
    • Almondsetat 1mo ago
      If you start with "I'm not a strong expert" maybe you should stop continuing saying wrong stuff. What you just wrote is completely wrong.
      • andriy_koval 1mo ago
        support your point with explanation or be ignored :-)
        • Almondsetat 1mo ago
          Godel proved that any system expressive enough to produce an arithmetic is incomplete. He initially proved it for the peano axioms but then it got generalized. ZFC can produce an arithmetic. Also, before being arrogant and demanding explanations, you should give them first for your claims
          • 1mo ago