Interesting approach. I just downloaded th *.mm file, and it ican be imported and verified by metamath.exe without problems. Since it is a huge file, I did not have a look at it in detail/at everything, but here are some remarks/questions: * to prefix wwfs with "w_" looks a little bit strange (example: `( w_ph -> ( w_ps -> w_ch ) )`): is there any reason for such prefixes? * are the axioms used identical with the axioms of set.mm? Is " The only major differences ... to set.mm is ax-13. " the only deviation? * I still cannot see any advantages (except the more formal namings) compared with set.mm.
[email protected] schrieb am Sonntag, 7. April 2024 um 01:59:48 UTC+2: > I organized it into chapters and gave theorems numbers. This is so they > can later accompany a PDF that contains meta-logical justifications > explains some things at a higher level. Read the heading for an explanation > of the notation I use for axiom / definition / theorem tags. My long term > goal is to write a Gödel numbering system. > > So far I've gotten through writing the logic section. Because I'm trying > to be more general, I'm not using the exact same approach as set.mm. The > only major differences seem to be with regard to set.mm's ax-13. So far > I've avoided the need for it by specifying that all ordinary object/set > variables are distinct. I can use term metavariables (which need not be > distinct from anything else) for the left side of definitions to make them > eliminable. ax-13 ( and ax-6 without a disjoint specification) don't hold > when terms can contain functions such as with the Peano Axioms. For > instance, `E. x x = t_t` doesn't hold unless you specify that `t_t` is > disjoint from `x`, because `t_t` could be `x + 1` `x = t_t` always false ( > I use a prefix 't_' and color green for terms ). set.mm uses classes > where terms would normally be used, but I can't really follow that path if > I'm not doing set theory. > > I have some more to talk about but would like to see if anyone is > interested before I go into more detail. I attached the file. -- 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/4918341f-d2cd-4bc8-a153-bfd9b6dd6c3bn%40googlegroups.com.
