Modelling Multiplicative Linear Logic via Deep Inference
<|reference_start|>Modelling Multiplicative Linear Logic via Deep Inference: Multiplicative linear logic is a very well studied formal system, and most such studies are concerned with the one-sided sequent calculus. In this paper we look in detail at existing translations between a deep inference system and the standard sequent calculus one, provide a simplified translation, and provide a formal proof that a standard approach to modelling is indeed invariant to all these translations. En route we establish a necessary condition for provable sequents related to the number of pars and tensors in a formula that seems to be missing from the literature.<|reference_end|>
@article{galor2024modelling,
    title={Modelling Multiplicative Linear Logic via Deep Inference},
    author={Tomer Galor and Andrea Schalk},
    journal={arXiv preprint arXiv:2404.01026},
    year={2024},
    archivePrefix={arXiv},
    eprint={2404.01026},
    primaryClass={math.LO cs.LO}
}