I had some other thoughts that I forgot to include: * Based on a technique I believe I learned from https://blog.plover.com/math/24-puzzle-2.html , it would seem at least plausible that I could syntactically encode associative-and-commutative structures as bags of some sort. I'm not sure if this is a worthwhile avenue of exploration, but I know at least one popular parenthesis-based language family, Lisp, does this for some associative operations.
* I wonder whether double-lollipop should be an additive or multiplicative conjunction. On Monday, May 20, 2019 at 12:02:23 PM UTC-7, fl wrote: > > It doesn't seem they have a decent set of axioms. You won't go very far. > > Totally understandable. Would there be a better set of axioms for doing this work? I don't know much about linear logic, and it seems like every author has a different presentation. Also, of course, if there's a preferred set of axioms that were waiting for some planned work along these same lines, then I'd prefer to go with what everybody else wants to do. How far should I expect to get? Is there some ceiling that you're anticipating? I'm hoping that, after I finish adding axioms and proving a base and doing some sanity checks, I'll be able to reach anything in set.mm. In particular, I've convinced myself of ~ ax-1 but with lollipops on a whiteboard, and I think (but am not sure) that ~ ax-2 is also valid in linear logic. It is hopefully a matter of typing, proving, and trying to remember the difference between the four connectives. -- 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/685fb46e-5dda-4fd6-acc2-8b183e876957%40googlegroups.com.
