Implementation of linear logic in Metamath
This is mostly a personal excercise in writing definitions and proofs in Metamath, as well as an excercise in getting an intuition for linear logic. However, you are welcome to use this database however you see fit.
There are currently several statements with no proof given. This is because I am still trying to decide on a good order and naming convention for the proofs. Once I settle on a system for arranging and naming the proofs, I’ll fill those in.
I’m not sure if the system I am using is entirely consistent, but if not, hey, it was fun while it lasted.
You can view the theorems right now, through the magic of modern technology. Check out the table of contents, or perhaps the list of all axioms and definitions.
If you want to inspect the raw database, install Metamath from http://us.metamath.org/ (or just open linear.mm in your favorite text editor). I recommend the mmj2 proof assistant if you want to try your hand at creating proofs, although it might be a little tricky to get up and running.
This project is written in the Metamath proof language, and takes heavy inspiration from Metamath’s primary database, set.mm.