Hypersequents and the Proof Theory of Intuitionistic Fuzzy Logic

TL;DR

This paper introduces a proof system for intuitionistic fuzzy logic using hypersequents, enabling sound, complete, and cut-elimination proofs, thus advancing the proof-theoretic understanding of this logic.

Contribution

It presents the first proof-theoretic calculus for intuitionistic fuzzy logic based on hypersequents, with proven soundness, completeness, and cut-elimination.

Findings

The system is sound and complete for intuitionistic fuzzy logic.

Cut-elimination is successfully established in the system.

The density rule's eliminability is confirmed.

Abstract

Takeuti and Titani have introduced and investigated a logic they called intuitionistic fuzzy logic. This logic is characterized as the first-order Goedel logic based on the truth value set [0,1]. The logic is known to be axiomatizable, but no deduction system amenable to proof-theoretic, and hence, computational treatment, has been known. Such a system is presented here, based on previous work on hypersequent calculi for propositional Goedel logics by Avron. It is shown that the system is sound and complete, and allows cut-elimination. A question by Takano regarding the eliminability of the Takeuti-Titani density rule is answered affirmatively.