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]. This paper introduces the method of density elimination by substitutions. 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 follows for many first-order fuzzy logics using a Dedekind–MacNeille-style completion and embedding.