On Thu, Jul 30, 2020 at 1:11 AM Raph Levien <[email protected]> wrote:
> A question: when translating to Lean, do you have to depend on classical > logic (ie "open classical"), or are you somehow able to avoid that? > Lean and metamath take a significantly different approach to axioms. In metamath, of course, there are many axioms, starting with classical propositional logic, then predicate logic, then the axioms of ZFC one at a time, with choice delayed to the last moment. In lean, there are only three axioms, but the "no axioms" baseline is very high (I'm not positive but I think it already exceeds ZFC in consistency strength), containing dependent type theory with inductive types and a hierarchy of universes. In lean, it is possible to build a model of ZFC as a certain inductive type. For obvious reasons, you need lean's choice to prove the ZFC choice axiom, but less obviously you also need it to prove replacement, because you have to choose a pre-set corresponding to each set in the mapping. (The ZFC model is a quotient by extensionality of an inductive type of pre-sets.) But choice actually gets involved much earlier, because the "no axioms" baseline of lean is only enough to get *intuitionistic* logic, not classical logic, and in lean the axiom of choice is used to prove the law of excluded middle. Since metamath assumes classical logic from the get-go, choice is therefore used in almost all translated theorems. Luckily, as a social matter, Leaners are used to not thinking about axiom usage at all; basically all of mathlib uses all three axioms and this system is basically equivalent to ZFC + countable inaccessible cardinals, so it is quite compatible with set.mm foundations. Mario > > On Wed, Jul 29, 2020 at 10:11 AM Mario Carneiro <[email protected]> wrote: > >> For those who might be interested, I just presented MM0 at the CICM >> conference, and the video is now on youtube: >> >> https://youtu.be/CxS0ONDfWJg >> >> (It occurs to me that I should have announced this *before* the talk, in >> case folks were interested in registering for free in order to attend >> directly. You can still ask questions here if you want.) >> >> Mario Carneiro >> >> -- >> You received this message because you are subscribed to the Google Groups >> "Metamath" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/metamath/CAFXXJSt_99WS9eusOuNv9iL%2BF665_APRLJQ9jVUqXzxer1GCZA%40mail.gmail.com >> <https://groups.google.com/d/msgid/metamath/CAFXXJSt_99WS9eusOuNv9iL%2BF665_APRLJQ9jVUqXzxer1GCZA%40mail.gmail.com?utm_medium=email&utm_source=footer> >> . >> > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/CADBEgNM6WD4rYwrFqJQ1sE5z%3DL%2BZAy2b7h5jyEqd0%2Bug%2BSaoeQ%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CADBEgNM6WD4rYwrFqJQ1sE5z%3DL%2BZAy2b7h5jyEqd0%2Bug%2BSaoeQ%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSuK_kLXjEaOQsCVCGFjDNmT9UjBfRtVz5e7a8D1ukPy9Q%40mail.gmail.com.
