On Thursday, July 9, 2020 at 4:41:43 PM UTC-4, Richard Penner wrote: > > > NM has stated (can't find where) that he would prefer not move my Frege > sections to the main set.mm. >
It was here: https://github.com/metamath/set.mm/pull/1604#issuecomment-618464178 > 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. > My basic objection was that it adds new axioms. set.mm was originally intended to show the derivation of ZFC theorems from a standard set of axioms, and I still think that should be its main purpose. Adding alternative axioms can be confusing and is probably not interesting to someone who just wants to get into the basics of set theory. Yesterday I took out the remaining alternate axioms in the prop/pred calc sections (that really shouldn't have been there) and moved most of them to my mathbox for now. Your work on Frege is very nice. I had mentioned the possibility of a separate .mm file and directory for it, but in addition to the work needed to create the auxiliary files, it wouldn't necessarily be as visible as having it in set.mm (for example new proofs would not show up on set.mm's Most Recent Proofs page). Instead, I have been thinking about putting all alternate axiomatizations at the end of the main part of set.mm (just before the start of mathboxes) in a new section called "Historical and alternate axiomatizations", along the lines of what I think FL had in mind. This will make it impossible for them to be used accidentally in the main part of set.mm,. Accidental use in mathboxes could still happen in principle, but "(New usage is discouraged.)" tags would largely prevent that, and anyway it would quickly be discovered whenever mathbox material is moved into the main part. (We can't add a new section after mathboxes without significant changes to metamath.exe, and anyway I'd rather keep to the simpler idea that mathboxes are at the end of set.mm.) Norm -- 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/e1f76afd-cb0a-41da-8efd-99870696eb57o%40googlegroups.com.
