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

DOI10.1007/978-3-030-36755-8_11MaRDI QIDQ2177586zbMATH OpenOpenAlexFDO

Authors Tim S. Lyon

Publication date 6 May 2020

Full work available at URL https://arxiv.org/abs/1910.06657

zbMATH Keywords

cut eliminationfuzzy logicGödel logicintuitionistic logiclinear nested sequentproof theory

Mathematics Subject Classification ID

Fuzzy logic; logic of vagueness (03B52) Cut-elimination and normal-form theorems (03F05)

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.

Review text

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].

Recommendations

• scientific article; zbMATH DE number 1670477
• A proof-theoretical investigation of global intuitionistic (fuzzy) logic
• Inducing syntactic cut-elimination for indexed nested sequents
• Cut elimination in nested sequents for intuitionistic modal logics
• Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents

Cited in

(2)

• Inducing syntactic cut-elimination for indexed nested sequents
• Internal and external calculi: ordering the jungle without being lost in translations

This page was built for publication: Syntactic cut-elimination for intuitionistic fuzzy logic via linear nested sequents

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2177586)