Skip to main content
SpringerLink
Log in

From Classical to Fuzzy Type Theory

  • Chapter
The Life and Work of Leon Henkin

Part of the book series: Studies in Universal Logic ((SUL))

  • 758 Accesses

Abstract

Higher-order logic—the type theory (TT)—is a powerful formal theory that has various kinds of applications, for example, in linguistic semantics, computer science, foundations of mathematics and elsewhere. It was proved to be incomplete with respect to standard models. In fifties and sixties of the last century, L. Henkin proved that there is an axiomatic system of TT that is complete if we relax the concept of model to the, so called, generalized one. The difference is that domains of functions in generalized models need not contain all possible functions but only subsets of them. Henkin then proved that a formula of type o (truth value) of a special theory T of the theory of types is provable iff it is true in all general models of T. Mathematical fuzzy logic is a special many-valued logic whose goal is to provide tools for capturing the vagueness phenomenon via degrees. It went through intensive development and many formal systems of both propositional as well as first-order fuzzy logic were proved to be complete. This endeavor was crowned in 2005 when also higher-order fuzzy logic (called the Fuzzy Type Theory, FTT) was developed and its completeness with respect to general models was proved. The proof is based on the ideas of the Henkin’s completeness proof for TT. This paper addresses several complete formal systems of the fuzzy type theory. The systems differ from each other by a chosen algebra of truth values. Namely, we focus on three systems: the Core FTT based on a special algebra of truth values for fuzzy type theory—the EQ-algebra, then IMTL-FTT based on IMTL Δ -algebra of truth values and finally the Ł-FTT based on MV Δ -algebra of truth values.

The research was supported by the European Regional Development Fund in the IT4 Innovations Centre of Excellence project (CZ.1.05/1.1.00/02.0070).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    In case of truth values, we speak about equivalence instead of equality.

  2. 2.

    A residuated lattice is accepted as the fundamental algebra of truth values considered in most systems of mathematical fuzzy logic.

  3. 3.

    As usual, we write m≗m′ instead of ≗(m,m′). The symbol [m≗m′] denotes an (arbitrary) truth value of m≗m′.

  4. 4.

    In the present literature on classical type theory, especially that focused on computer science, the formulas are often called lambda-terms. We will keep the original logical term introduced by A. Church and L. Henkin to emphasize that we are developing the logic.

  5. 5.

    Such a theory in [16] and also in [27] is called complete.

  6. 6.

    To be precise, the resulting type theory is isomorphic with the classical simple theory of types.

References

  1. Andrews, P.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Kluwer Academic, Dordrecht (2002)

    Book  Google Scholar 

  2. Chang, C.C.: Algebraic analysis of many valued logics. Trans. AMS 93, 74–80 (1958)

    Google Scholar 

  3. Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5, 56–68 (1940)

    Article  MathSciNet  Google Scholar 

  4. Cignoli, R.L.O., D’Ottaviano, I.M.L., Mundici, D.: Algebraic Foundations of Many-Valued Reasoning. Kluwer Academic, Dordrecht (2000)

    Book  MATH  Google Scholar 

  5. Cintula, P., Esteva, F., Gispert, J., Godo, L., Noguera, C.: Distinguished algebraic semantics for t-norm based fuzzy logics: methods and algebraic equivalencies. Ann. Pure Appl. Log. 160, 53–81 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  6. Cintula, P., Hájek, P., Horčík, R.: Formal systems of fuzzy logic and their fragments. Ann. Pure Appl. Log. 150, 40–65 (2007)

    Article  MATH  Google Scholar 

  7. Cintula, P., Hájek, P., Noguera, C. (eds.): Handbook of Mathematical Fuzzy Logic, vol. 1. College Publications, London (2011)

    Google Scholar 

  8. Cintula, P., Hájek, P., Noguera, C. (eds.): Handbook of Mathematical Fuzzy Logic, vol. 2. College Publications, London (2011)

    Google Scholar 

  9. Duží, D., Jespersen, B., Materna, P.: Procedural Semantics for Hyperintensional Logic. Springer, Dordrecht (2010)

    MATH  Google Scholar 

  10. Dyba, M., Novák, V.: EQ-logics: non-commutative fuzzy logics based on fuzzy equality. Fuzzy Sets Syst. 172, 13–32 (2011)

    Article  MATH  Google Scholar 

  11. Esteva, F., Godo, L.: Monoidal t-norm based logic: towards a logic for left-continuous t-norms. Fuzzy Sets Syst. 124, 271–288 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  12. Farmer, W.M.: A partial functions version of Church’s simple theory of types. J. Symb. Log. 55, 1269–1291 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  13. Gallin, D. (ed.): Intensional and Higher-Order Modal Logic (with Applications to Montague Semantics). North-Holland, Amsterdam (1975)

    MATH  Google Scholar 

  14. Goguen, J.A.: The logic of inexact concepts. Synthese 19, 325–373 (1968–1969)

    Article  Google Scholar 

  15. Gottwald, S.: A Treatise on Many-Valued Logics. Research Studies Press Ltd., Baldock, Herfordshire (2001)

    MATH  Google Scholar 

  16. Hájek, P.: Metamathematics of Fuzzy Logic. Kluwer Academic, Dordrecht (1998)

    Book  MATH  Google Scholar 

  17. Hájek, P.: Fuzzy logics with noncommutative conjunctions. J. Log. Comput. 13, 469–479 (2003)

    Article  MATH  Google Scholar 

  18. Henkin, L.: Completeness in the theory of types. J. Symb. Log. 15, 81–91 (1950)

    Article  MathSciNet  MATH  Google Scholar 

  19. Henkin, L.: A theory of propositional types. Fundam. Math. 52, 323–344 (1963)

    MathSciNet  MATH  Google Scholar 

  20. Klement, E.P., Mesiar, R., Pap, E.: Triangular Norms. Kluwer Academic, Dordrecht (2000)

    Book  MATH  Google Scholar 

  21. Łukasiewicz, L.: O logice trojwartoscowej. (On three-valued logic). Ruch Filoz. 5, 170–171 (1920) (in Polish)

    Google Scholar 

  22. Łukasiewicz, L., Borkowski, L.: Selected Works, Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam (1970)

    Google Scholar 

  23. Materna, P.: Concepts and Objects. Acta Philosophica Fennica, vol. 63, Helsinki (1998)

    Google Scholar 

  24. Materna, P.: Conceptual Systems. Logos Verlag, Berlin (2004)

    MATH  Google Scholar 

  25. Novák, V.: Fuzzy Sets and Their Applications. Adam Hilger, Bristol (1989)

    MATH  Google Scholar 

  26. Novák, V.: Towards fuzzy type theory. In: Proc. Int. Seminar on Multiple-Valued Logic ISMVL 2003, pp. 65–70. Meiji Univ. Tokyo, Tokyo (2003)

    Chapter  Google Scholar 

  27. Novák, V.: On fuzzy type theory. Fuzzy Sets Syst. 149, 235–273 (2005)

    Article  MATH  Google Scholar 

  28. Novák, V.: A comprehensive theory of trichotomous evaluative linguistic expressions. Fuzzy Sets Syst. 159(22), 2939–2969 (2008)

    Article  MATH  Google Scholar 

  29. Novák, V.: EQ-algebra-based fuzzy type theory and its extensions. Log. J. IGPL 19, 512–542 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  30. Novák, V.: Reasoning about mathematical fuzzy logic and its future. Fuzzy Sets Syst. 192, 25–44 (2012)

    Article  MATH  Google Scholar 

  31. Novák, V., de Baets, B.: EQ-algebras. Fuzzy Sets Syst. 160, 2956–2978 (2009)

    Article  MATH  Google Scholar 

  32. Novák, V., Pavliska, V., Perfilieva, I., Štěpnička, M.: F-transform and fuzzy natural logic in time series analysis. In: Proc. Int. Conference EUSFLAT-LFA’2013, Milano, Italy (2013)

    Google Scholar 

  33. Novák, V., Perfilieva, I. (eds.): Discovering the World with Fuzzy Logic. Studies in Fuzziness and Soft Computing, vol. 57. Springer, Heidelberg (2000)

    MATH  Google Scholar 

  34. Novák, V., Perfilieva, I., Močkoř, J.: Mathematical Principles of Fuzzy Logic. Kluwer Academic, Boston (1999)

    Book  MATH  Google Scholar 

  35. Pavelka, J.: On fuzzy logic I, II, III. Z. Math. Log. Grundl. Math. 25, 45–52 (1979). Also see pp. 119–134, 447–464

    Article  MathSciNet  MATH  Google Scholar 

  36. Russell, B.: Mathematical logic as based on the theory of types. Am. J. Math. 30, 222–262 (1908)

    Article  MATH  Google Scholar 

  37. Tichý, P.: The Foundations of Frege’s Logic. De Gruyter, Berlin (1988)

    Book  MATH  Google Scholar 

  38. Zadeh, L.A.: Fuzzy sets. Inf. Control 8, 338–353 (1965)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute for Research and Applications of Fuzzy Modelling, National Supercomputing Centre IT4 Innovations, University of Ostrava, 30. dubna 22, 701 03, Ostrava 1, Czech Republic

    Vilém Novák

Authors
  1. Vilém Novák
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Vilém Novák .

Editor information

Editors and Affiliations

  1. Department of Philosophy, Logic and Aesthetics, University of Salamanca, Salamanca, Spain

    María Manzano

  2. Alfréd Rényi Institute of Mathematics, Hungarian Academy of Sciences, Budapest, Hungary

    Ildikó Sain

  3. Department of Logic and Philosophy of Science, Autonomous University of Madrid, Madrid, Spain

    Enrique Alonso

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Novák, V. (2014). From Classical to Fuzzy Type Theory. In: Manzano, M., Sain, I., Alonso, E. (eds) The Life and Work of Leon Henkin. Studies in Universal Logic. Birkhäuser, Cham. https://doi.org/10.1007/978-3-319-09719-0_16

Download citation

Publish with us

Policies and ethics

Search

Navigation