A Natural Deduction System for Intuitionistic Fuzzy Logic

  • Matthias Baaz
  • Agata Ciabattoni
  • Christian G. Fermüller
Part of the Advances in Soft Computing book series (AINSC, volume 11)


Intuitionistic fuzzy logic IF was introduced by Takeuti and Titani. This logic coincides with the first-order Gödel logic based on the real unit interval [0,1] as set of truth-values. We present a natural deduction system NIF for IF. NIF is defined by suitably translating a first-order extension of Avron’s hypersequent calculus for Gödel logic. Soundness, completeness and normal form theorems for NIF are provided.


Deduction System Intuitionistic Logic Natural Deduction Sequent Calculus Derivation Tree 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Avellone, A., Ferrari, M. and Miglioli P.: Duplication-free tableau calculi together with cut-free and contraction free sequent calculi for the interpolable propositional intermediate logics. Logic Journal of the IGPL, 7(4) (1999), 447–480.MathSciNetMATHCrossRefGoogle Scholar
  2. 2.
    Avron, A.: Hypersequents, logical consequence and intermediate logics for con-currency. Annals for Mathematics and Artificial Intelligence, 4 (1991), 225–248.MathSciNetMATHCrossRefGoogle Scholar
  3. 3.
    Avron, A.: The method of hypersequents in the proof theory of propositional nonclassical logics. In Logic: from Foundations to Applications, European Logic Colloquium, Oxford Science Publications. Clarendon Press. Oxford, 1996, 1–32.Google Scholar
  4. 4.
    Baaz, M., Ciabattoni A., Fermüller, C.G., Veith, H.: On the Undecidability of Some Sub-classical First-Order Logics. Proceedings of FSTTCS’99. LNCS 1738, 1999, 258–268.Google Scholar
  5. 5.
    Baaz, M., Fermüller, C.G., Zach, R.: Systematic Construction of Natural Deduction Systems for Many-valued logics. In: Proc. 23th International Symposium on Multiple-Valued Logics. Los Gatos, CA. IEEE Press. 1993, 208–213.Google Scholar
  6. 6.
    Haag, M., Veith, H.: An Axiomatization of Quantified Propositional Gödel Logic Using the Takeuti-Titani Rule. Proc. Logic Colloquium 1998, Lecture Notes in Logic, ASL, 2000.Google Scholar
  7. 7.
    Baaz, M., Zach, R.: Hypersequents and the Proof Theory of Intuitionistic Fuzzy Logic. Proc. CSL’2000, 2000, 187–201.Google Scholar
  8. 8.
    Dyckhoff, R.: A Deterministic Terminating Sequent Calculus for GödelDummett logic. Logic Journal of the IGPL, 7 (1999), 319–326.MathSciNetMATHCrossRefGoogle Scholar
  9. 9.
    Dummett, M.: A propositional calculus with denumerable matrix. J. Symbolic Logic, 24 (1959), 97–106.MathSciNetMATHCrossRefGoogle Scholar
  10. 10.
    Gentzen, G.: Untersuchungen über das logische Schliessen I, II. Mathematische Zeitschrift, 39 (1934–35), 176–210, 405–431.Google Scholar
  11. 11.
    Gödel, K.: Zum intuitionistischen Aussagenkalkül. Anz. Akad. Wiss. Wien, 69 (1932), 65–66.MATHGoogle Scholar
  12. 12.
    Hâjek, P.: Metamathematics of Fuzzy Logic. Kluwer, 1998.Google Scholar
  13. 13.
    Horn, A.: Logic with truth values in a linearly ordered Heyting algebra. J. Symbolic Logic, 27 (1962), 159–170.MathSciNetCrossRefGoogle Scholar
  14. 14.
    Prawitz, D.: Natural Deduction: A Proof Theoretical Study. Almquist and Wiksell. 1965.Google Scholar
  15. 15.
    Prawitz, D.: Ideas and results in proof theory. In Proceedings of the Second Scandinavian Logic Symposium, North-Holland, Amsterdam, 1971, 235–307.CrossRefGoogle Scholar
  16. 16.
    Sonobe, O.: A Gentzen-type Formulation of Some Intermediate Propositional Logics. J. of Tsuda College, 7 (1975), 7–14.MathSciNetGoogle Scholar
  17. 17.
    Tait, W.W.: Normal derivability in classical logic. In: The Syntax and Semantics of infinitary Languages. J. Barwise ed., Lectures Notes in Mathematics, Springer, Berlin. 72 (1968), 204–236.CrossRefGoogle Scholar
  18. 18.
    Takeuti, G., Titani, S.: Intuitionistic fuzzy logic and intuitionistic fuzzy set theory. J. of Symbolic Logic, 49 (1984), 851–866.MathSciNetMATHCrossRefGoogle Scholar
  19. 19.
    Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science 43. Cambridge, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Matthias Baaz
    • 1
  • Agata Ciabattoni
    • 1
  • Christian G. Fermüller
    • 2
  1. 1.Institut für Algebra und Computermathematik E118.2Technische Universität WienViennaAustria
  2. 2.Institut für Computersprachen E185Technische Universität WienViennaAustria

Personalised recommendations