Formalization of Chapter 2 of "An Introduction to Substructural Logics" by Greg Restall. Developed by Matthew LeBar at University of Chicago with supervision by Professor Stuart Kurtz.