×

Density elimination. (English) Zbl 1206.03027

Summary: 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.

MSC:

03B52 Fuzzy logic; logic of vagueness
03F05 Cut-elimination and normal-form theorems
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Avron, A., A constructive analysis of RM, Journal of Symbolic Logic, 52, 4, 939-951 (1987) · Zbl 0639.03017
[2] Avron, A., Hypersequents, logical consequence and intermediate logics for concurrency, Annals of Mathematics and Artificial Intelligence, 4, 3-4, 225-248 (1991) · Zbl 0865.03042
[3] Baaz, M.; Ciabattoni, A.; Montagna, F., Analytic calculi for monoidal t-norm based logic, Fundamenta Informaticae, 59, 4, 315-332 (2004) · Zbl 1057.03019
[4] Baaz, M.; Zach, R., Hypersequents and the proof theory of intuitionistic fuzzy logic, (Clote, P.; Schwichtenberg, H., Proceedings of CSL 2000. Proceedings of CSL 2000, LNCS, vol. 1862 (2000), Springer), 187-201 · Zbl 0973.03029
[5] Ciabattoni, A., Automated generation of analytic calculi for logics with linearity, (Marcinkowski, J.; Tarlecki, A., Proceedings of CSL 2004. Proceedings of CSL 2004, LNCS, vol. 3210 (2004), Springer), 503-517 · Zbl 1095.68109
[6] Ciabattoni, A.; Esteva, F.; Godo, L., T-norm based logics with \(n\)-contraction, Neural Network World, 12, 5, 441-453 (2002)
[7] Ciabattoni, A.; Metcalfe, G., Density elimination and rational completeness for first order logics, (Artëmov, S.; Nerode, A., Proceedings of LFCS 2007. Proceedings of LFCS 2007, LNCS, vol. 4514 (2007), Springer), 132-146 · Zbl 1133.03028
[8] Cintula, P.; Hájek, P., On theories and models in fuzzy predicate logics, Journal of Symbolic Logic, 71, 3, 832-863 (2006) · Zbl 1111.03030
[9] Esteva, F.; Gispert, J.; Godo, L.; Montagna, F., On the standard and rational completeness of some axiomatic extensions of the monoidal t-norm logic, Studia Logica, 71, 2, 199-226 (2002) · Zbl 1011.03015
[10] Esteva, F.; Godo, L., Monoidal t-norm based logic: Towards a logic for left-continuous t-norms, Fuzzy Sets and Systems, 124, 271-288 (2001) · Zbl 0994.03017
[11] Hájek, P., Metamathematics of Fuzzy Logic (1998), Kluwer: Kluwer Dordrecht · Zbl 0937.03030
[12] Hart, J.; Rafter, L.; Tsinakis, C., The structure of commutative residuated lattices, International Journal of Algebra and Computation, 12, 4, 509-524 (2002) · Zbl 1011.06006
[13] Horn, A., Logic with truth values in a linearly ordered Heyting algebra, Journal of Symbolic Logic, 34, 3, 395-409 (1969) · Zbl 0181.29904
[14] Jenei, S.; Montagna, F., A proof of standard completeness for Esteva and Godo’s MTL logic, Studia Logica, 70, 2, 183-192 (2002) · Zbl 0997.03027
[15] Metcalfe, G.; Montagna, F., Substructural fuzzy logics, Journal of Symbolic Logic, 7, 3, 834-864 (2007) · Zbl 1139.03017
[16] Montagna, F.; Ono, H., Kripke semantics, undecidability and standard completeness for Esteva and Godo’s logic MTL \(\forall \), Studia Logica, 71, 2, 227-245 (2002) · Zbl 1013.03021
[17] Takano, M., Another proof of the strong completeness of the intuitionistic fuzzy logic, Tsukuba J. Math., 11, 851-866 (1984)
[18] Takeuti, G.; Titani, T., Intuitionistic fuzzy logic and intuitionistic fuzzy set theory, Journal of Symbolic Logic, 49, 3, 851-866 (1984) · Zbl 0575.03015
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.