Syntactic cut-elimination for intuitionistic fuzzy logic via linear nested sequents (Q2177586)

In this paper, the author introduces a cut-free calculus, called LNIF, by applying to intuitionistic fuzzy logic (IF) the linear nested sequent framework introduced by \textit{B. Lellmann} [Lect. Notes Comput. Sci. 9323, 135--150 (2015; Zbl 1471.03080)]. After a detailed introduction including a quick overview on other sequent calculi for IF, the author recalls the axiomatization and the semantics of IF as presented in \textit{D. M. Gabbay} et al. [Quantification in nonclassical logic. Volume I. Amsterdam: Elsevier (2009; Zbl 1211.03002)]. Sections 3 and 4 are the most strictly technical ones. In Section 3, he introduces the LNIF calculus and proves its soundness and completeness w.r.t. IF, while in Section 4 the main properties of LNIF are proved. Such a calculus enjoys the properties of separation, symmetry, internality, cut elimination, subformula property, admissibility of structural rules, and invertibility of rules. Last, the author concludes the paper by discussing possible future works and further applications of LNIF calculus, e.g., a midsequent theorem and interpolation. For the entire collection see [Zbl 1428.03004].