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

TL;DR

This paper introduces a new linear nested sequent calculus for intuitionistic fuzzy logic, enabling cut-elimination and proving key proof-theoretic properties, advancing the proof theory of fuzzy logic systems.

Contribution

The paper develops the first linear nested sequent calculus for intuitionistic fuzzy logic, demonstrating cut-elimination and other proof-theoretic properties.

Findings

The calculus LNIF is cut-free and invertible.

All structural rules are admissible in LNIF.

The framework supports syntactic cut-elimination.

Abstract

This paper employs the linear nested sequent framework to design a new cut-free calculus LNIF for intuitionistic fuzzy logic--the first-order G\"odel 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 invertibility of all rules, admissibility of structural rules, and syntactic cut-elimination.