Syntactic Cut-Elimination for Intuitionistic Fuzzy Logic via Linear Nested Sequents

摘要

This paper employs the linear nested sequent framework to design a new cut-free calculus (LNIF) for intuitionistic fuzzy logic?the first-order Godel logic characterized by linear relational frames with constant domains. Linear nested sequents?which are nested sequents restricted to linear structures?prove to be a well-suited proof-theoretic formalism for intuitionistic fuzzy logic. We show that the calculus LNIF possesses highly desirable proof-theoretic properties such as invertibil-ity of all rules, admissibility of structural rules, and syntactic cut-elimination.