> 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?
On Thu, 30 Jul 2020 11:13:56 +0200, Mario Carneiro <[email protected]> wrote: > 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. ... Clarification: Mario is talking here about the *set.mm* metamath database, not about metamath in general, since obviously metamath can be used without using classical logic or ZFC simply by creating a different database. Mario's extremely well aware of that, and is an expert on that topic, but I thought other readers here might be confused. --- David A. Wheeler -- 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/E1k1Aik-0001Yh-VP%40rmmprod06.runbox.
