Formalization (ax-frege1 through frege133) has been completed and is on the recent proofs page.
What's new is that I have revised statements to embrace class variables as widely as possible for frege70 and later. Quite often this means there is also a corresponding element hypothesis for each as most of these class variables are required to be sets. Formalizing some of Frege's substitutions led to the introduction of the union. frege109 and frege130 will really test your ability to convert between the two notations. Proving dffrege76 was the most challenging part. NM has stated (can't find where) that he would prefer not move my Frege sections to the main set.mm. I think his preference was for partition of hereditary and Frege from set.mm if the website supported it. Perhaps he may warm to FL's proposal. I am happy that we got some of the work on transitive closure of relations into the main section. My November notes on Frege were lengthy and complex without the t+ function. -- 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/0fdd461e-8088-4bcc-9168-d9fb33d2bb29o%40googlegroups.com.
