I'm reading the formalization of Frege's *Begriffsschrift* . I'm in favor of formalizing the most famous mathematical works of the past. Currently there are four of them. Wheeler's works on scholastic and stoic logics, Frege's *Begriffsschrift * and eventually the Principles of Euclid proposed by myself. In my opinion these works shouldn't be aggregated with the rest of set.mm but kept separate in their own sections. They should come with precise references to the original texts. They should be conceived as a tool for reading these texts which no longer belong to living mathematics but are a part of its past and as such are necessary to understand how we got to where we are. They might be considered as a help to understand texts that are otherwise difficult to read because of symbols, terms and other features that are outdated. They might be placed after the official sections in annex ones.
-- FL -- 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/8d4ac5ac-932f-46a2-b56d-f6c67acee26eo%40googlegroups.com.
