View article

This paper employs the linear nested sequent framework to design a new cut-free calculus () for intuitionistic fuzzy logic—the first-order Gödel 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 possesses highly desirable proof-theoretic properties such as invertibility of all rules, admissibility of structural rules, and syntactic cut-elimination.