Hello, As an excercise in both linear logic and writing Metamath databases, I am making a formalization of linear logic in Metamath The .mm file is here: https://github.com/ishanpm/metamathlinear/blob/master/linear.mm. The axiomatization I am using is based on *Axioms and Models of Linear Logic* by Wim H. Hesselink: https://www.rug.nl/research/portal/files/3359896/1990FormAspCompHesselink2.pdf. I know I'm not the only person doing something like this, but I wanted some feedback on what I have so far.
I am still trying to decide on good conventions for the names and order of the proofs. Do you have any advice for me regarding this? The naming is currently somewhat inconsistent since I am trying several things at once. -- 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/ce8d9dac-b4a4-43b0-a1b8-904deda77c95%40googlegroups.com.
