Soundness and completeness are not enough

This blog post is based on a talk recently given at Chapman University, developed within the context of our joint Topos–Chapman collaboration. I thank the audience for a lively discussion. Milly Maietti In the 1990s, intuitionistic linear logic was booming. There were multiple typed calculi, multiple categorical models, and a growing body of results showing soundness and completeness between them. Everything looked harmonious. But something subtle was wrong. In a joint paper with Maria Emilia Ma