Hi! I've started work on what I'm thinking of as "lset.mm": https://gist.github.com/3e1cfa0062bed748234f573558211869
I have a few thoughts, both about Metamath and about this particular adventure: * I tried several different flavors of syntax before picking this one. I tried having sequent-style symmetric turnstiles, but that had terrible bookkeeping problems. I thought about postfix negation, as is traditional for linear logic (it looks like exponentiation with _|_ ) but I had trouble writing the rules. (I am stopping myself from writing a Metamath syntax compiler.) * As a category-theoretic desire, I'd like to be able to enter isomorphisms as axioms without incurring a double-entry penalty. I'd also like to not have to define both introduction and elimination axioms for new syntax built on old connectives. * Relatedly, I want to have to only express a single associative law for each connective. Digging down into parens is unpleasant. I was considering weakening the turnstile at the head of those axioms to `wff` or something along those lines, but I'm not yet thinking enough like the Metamath parser to be able to predict what will go wrong with that. (As a language designer, this is screaming to me "you're putting too much into the syntax", but aren't we putting *everything* into the syntax?) * set.mm rushes to set up implication and then to move deduction into the object language, where we have more powerful deductive tools. However, implication is not as primitive in (classical) linear logic, and is honestly more pleasantly defined in terms of the multiplicative connectives; this not only leaves a gap before the introduction of implication, but cannot solve all upcoming issues since the additive connectives do not interact well with implication. Further, in this file so far, it seems like I can apply ~ ax-i or ~ id in order to convert the Metamath-level rules into lollipops. Maybe this isn't a big deal, just a matter of ergonomics and my own inexperience. * ⅋ is not in ASCII and there appears to be no good replacement. On the plus side, maybe this will lead to a demystification of this operator. * Nomenclature is difficult, as always. * This was a little hard, but mostly what is hard is looking at nearly 600KLOC of set.mm and trying to imagine how much of that I'll be able to get to. I know that there's a lot of intermediate stuff that I can pick and choose to prove, depending on where I'm going, but I haven't even reached the integers. * I need to replace 0 and 1, probably, if I *do* reach the integers. Z and O maybe? * I'm not a mathematician. This is probably a problem, or at least problematic. * The proof assistant is alright. I'm able to integrate it with my editor somewhat, and to prove one or two proofs at a time, slowly. * Proof verification is so fast that it changes how I'm thinking about my workflow compared to other languages like Coq. Thanks, ~ C. -- 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/e3c7e164-998e-4c56-83e0-35e5d19d1e88%40googlegroups.com.
