A focused linear logical framework and its application to metatheory of object logics. (15th March 2021)

• Record Type: Journal Article
• Authors: Felty, Amy; Olarte, Carlos; Xavier, Bruno
• Is Part Of: Mathematical structures in computer science. Volume 31:Number 3(2021)
• Page Start: 312
• Page End: 340
• Publication Date: 2021-03-15
• Subjects: Linear logic -- cut-elimination -- focusing -- Coq; Computer science -- Mathematics -- Periodicals; 004.015105
• DOI: 10.1017/S0960129521000323
• Languages: English
• ISSNs: 0960-1295

Abstract

Abstract: Linear logic (LL) has been used as a foundation (and inspiration) for the development of programming languages, logical frameworks, and models for concurrency. LL's cut-elimination and the completeness of focusing are two of its fundamental properties that have been exploited in such applications. This paper formalizes the proof of cut-elimination for focused LL. For that, we propose a set of five cut-rules that allows us to prove cut-elimination directly on the focused system. We also encode the inference rules of other logics as LL theories and formalize the necessary conditions for those logics to have cut-elimination. We then obtain, for free, cut-elimination for first-order classical, intuitionistic, and variants of LL. We also use the LL metatheory to formalize the relative completeness of natural deduction and sequent calculus in first-order minimal logic. Hence, we propose a framework that can be used to formalize fundamental properties of logical systems specified as LL theories.