This seems very useful for understanding the Frege notation. I can add it to the mpeuni directory. However, the mmfrege.html file should pass http://validator.w3.org, and the main header should be centered like on the other website pages. Also, there are a large number of separate svg files; perhaps you can prefix the svg file names with "_frege_" so they can be more easily identified. Currently we are keeping svg files in the same directory as html files (perhaps not the greatest practice, but it's what the site creation scripts currently expect), so the you would reference "fregenotation/jABinS.svg" as "_frege_jABinS.svg" in the html file.
For referencing mmfrege.html in a set.mm comment, you can use "~ mmfrege.html". The "mm" prefix identifies it as something other than a set.mm label (labels beginning with "mm" are not allowed by "verify markup"). Norm On Monday, November 2, 2020 at 9:47:43 AM UTC-5 [email protected] wrote: > Not dead! > > Back in July, I mined Frege's original work on triple disjunction and > conjunction and just last night got them into a PR. > > I looked into SVG to reproduce Frege's original notation for the web, and > created a mmfrege.raw.html to give examples comparing both the notation and > possible idiomatic translations which use set.mm's wider range of > notations. Attached is a zip file with the SVG and metamath-processed > output file mmfrege.html and a PDF. > > On Saturday, July 11, 2020 at 9:15:03 AM UTC-7 Norman Megill wrote: > >> 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/80a68083-2c07-4d11-b9a5-27480f8cad22n%40googlegroups.com.
