Density elimination

Density elimination, a close relative of cut elimination, consists of removing applications of the Takeuti-Titani density rule from derivations in Gentzen-style (hypersequent) calculi. Its most important use is as a crucial step in establishing standard completeness for syntactic presentations of fuzzy logics; that is, completeness with respect to algebras based on the real unit interval [0, 1]. In this paper, the method of density elimination by substitutions is introduced. For general classes of (first-order) hypersequent calculi, it is shown that density elimination by substitutions is guaranteed by known sufficient conditions for cut elimination. These results provide the basis for uniform characterizations of calculi complete with respect to densely and linearly ordered algebras. Standard completeness then follows for many firstorder fuzzy logics using a Dedekind-MacNeille-style construction. Key words: Hypersequents, sequents, cut elimination, density elimination, substructural ...

• Type: Journal
• Year: 2008
• Where: TCS
• Authors: Agata Ciabattoni, George Metcalfe
• Keywords: Density Elimination, Fuzzy Logics, Standard Completeness, TCS 2008, Theoretical Computer Science