On Fri, 3 Jul 2020 05:21:38 -0700 (PDT), "'fl' via Metamath" <[email protected]> wrote: > I'm reading the formalization of Frege's *Begriffsschrift* . I'm in favor > of formalizing the most famous mathematical > works of the past.
Sounds good! I love mathematical history, and it's definitely true that older works can be hard to understand. Principia Mathematica's notation still gives me a headache, and that's in the recent past, that's barely over 100 years ago. > In my opinion > these works shouldn't be aggregated with the > rest of set.mm but kept separate in their own sections. I think we should *not* have such a rigid rule, at least in the sense that we should definitely allow famous axioms & results in the main body: - A lot of current mathematics builds on past works. It'd be impossible to *only have such works later. - Specific old expressions turn out to have surprising utility; stoic3 is now used in 71 theorems. - There are multiple possible goals. I proved (just) the Stoic indemonstrables and Aristotelian syllogisms early, but for different reasons. Proving them early is a good way to demonstrate that the axioms used in set.mm are at least as strong as those used by these other works. I think demonstrating that early is important, and they don't take a lot of space because I made no attempt to prove "everything" from older works. > They might be placed after > the official sections in annex ones. I think that would make more sense. These sections could formalize older works, and include comments where certain results are already proven in the main body. One challenge is that you will often NOT be able to precisely record exactly the meanings of the older/other works in a simple way in set.mm, because their axiom systems & logic are NOT identical to set.mm. For example, to (mis)use modern terminology, Aristotelian logic only permits non-empty sets; a common solution (which I applied) is to require "there exists" in just the specific cases it requires. That may be okay, because that provides a springboard for comparing our (more modern) system with theirs, and in some sense a translation of it. But if you want to precisely capture their logic, I think that in at least some cases you'll need to create a new database. --- 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/E1jrO3y-0001Ie-Sd%40rmmprod06.runbox.
