Skip to main content
SpringerLink
Log in

An Equational Re-engineering of Set Theories

  • Conference paper
  • First Online:
Automated Deduction in Classical and Non-Classical Logics (FTP 1998)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1761))

Included in the following conference series:

Abstract

New successes in dealing with set theories by means of state-of-the-art theorem-provers may ensue from terse and concise axiomatizations, such as can be moulded in the framework of the (fully equational) Tarski-Givant map calculus. In this paper we carry out this task in detail, setting the ground for a number of experiments.

This is hence the advantage of our method: that immediately ... and with the only guidance of characters and through a safe and really analytic method, we bring to light truths that others had barely achieved by an immense mind effort and by chance. And therefore we are able to present within our century results which, otherwise, the course of many thousands of years would hardly deliver. (G. W. Leibniz, 1679)

Work partially supported by the CNR of Italy, coordinated project SETA, and by MURST 40%, “Tecniche speciali per la specifica, l’analisi, la verifica, la sintesi e la trasformazione di programmi”.

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P. B. Andrews, D. Miller, E. Longini Cohen, and F. Pfenning. Automating higher-order logic. In W. W. Bledsoe and D. W. Loveland eds., Automated theorem proving: After 25 years, 169–192. American Mathematical Society, Contemporary Mathematics vol.29, 1984.

    Google Scholar 

  2. S. C. Bailin and D. Barker-Plummer. \( \mathcal{Z} \) -match: An inference rule for incrementally elaborating set instantiations. J. Automated Reasoning, 11(3):391–428, 1993. (Errata in J. Automated Reasoning, 12(3):411–412, 1994).

    Article  MATH  MathSciNet  Google Scholar 

  3. J. G. F. Belinfante. On a modification of Gödel’s algorithm for class formation. AAR Newsletter No.34, 10–15, 1996.

    Google Scholar 

  4. R. Boyer, E. Lusk, W. McCune, R. Overbeek, M. Stickel, and L. Wos. Set theory in first-order logic: Clauses for Gödel’s axioms. J. Automated Reasoning, 2(3):287–327, 1986.

    Article  MATH  Google Scholar 

  5. D. Cantone, A. Cavarra, and E. G. Omodeo. On existentially quantified conjunctions of atomic formulae of \( \mathcal{L}^ + \) . In M. P. Bonacina and U. Furbach, eds., Proc. of the FTP97 International workshop on first-order theorem proving, RISC-Linz Report Series No.97-50, pp. 45–52, 1997.

    Google Scholar 

  6. D. Cantone, A. Ferro, and E. G. Omodeo. Computable set theory. Vol. 1. Int. Series of Monographs on Computer Science. Oxford University Press, 1989.

    Google Scholar 

  7. P. J. Cohen. Set Theory and the continuum hypothesis. Benjamin, New York, 1966.

    MATH  Google Scholar 

  8. I. Düntsch. Rough relation algebras. Fundamenta Informaticae, 21:321–331, 1994.

    MATH  MathSciNet  Google Scholar 

  9. A. Formisano, E. G. Omodeo, and M. Temperini. Plan of activities on the map calculus. In J. L. Freire-Nistal, M. Falaschi, and M. Vilares Ferro, eds., Proc. of the AGP98 Joint Conference on Declarative Programming, pp. 343–356, A Coruña, Spain, 1998.

    Google Scholar 

  10. M. F. Frias, A. M. Haeberer, and P. A. S. Veloso. A finite axiomatization for fork algebras. J. of the IGPL, 5(3):311–319, 1997.

    MATH  MathSciNet  Google Scholar 

  11. S. R. Givant. The Structure of Relation Algebras Generated by Relativization, volume 156 of Contemporary Mathematics. American Mathematical Society, 1994.

    Google Scholar 

  12. D. Gries and F. B. Schneider. A logical approach to discrete math. Texts and Monographs in Computer Science. Springer-Verlag, 1994.

    Google Scholar 

  13. A. M. Haeberer, G. A. Baum, and G. Schmidt. On the smooth calculation of relational recursive expressions out of first-order non-constructive specifications involving quantifiers. In Proc. of the International Conference on Formal Methods in Programming and their Applications. LNCS 735:281–298. Springer-Verlag, 1993.

    Chapter  Google Scholar 

  14. T. J. Jech Set theory, Academic Press, New York, 1978.

    Google Scholar 

  15. B. Jónsson and A. Tarski. Representation problems for relation algebras. Bull. Amer. Math. Soc., 54, 1948

    Google Scholar 

  16. J.-L. Krivine Introduction to axiomatic set theory, Reidel, Dordrecht. Holland, 1971.

    MATH  Google Scholar 

  17. R. C. Lyndon The representation of relational algebras. Annals of Mathematics, 51(3):707–729, 1950.

    Article  MathSciNet  Google Scholar 

  18. W. W. McCune. Otter 3.0 reference manual and guide. Technical Report ANL-94/6, Argonne National Laboratory, 1994. (Revision A, august 1995).

    Google Scholar 

  19. Ph. A. J. Noël. Experimenting with Isabelle in ZF set theory. J. Automated Reasoning, 10(1):15–58, 1993.

    Article  MATH  Google Scholar 

  20. E. G. Omodeo and A. Policriti. Solvable set/hyperset contexts: I. Some decision procedures for the pure, finite case. Comm. Pure App. Math., 48(9–10):1123–1155, 1995. Special Issue in honor of J.T. Schwartz.

    Article  MATH  MathSciNet  Google Scholar 

  21. E. Orlowska. Relational semantics for nonclassical logics: Formulas are relations. In Wolenski, J. ed. Philosophical Logic in Poland, pages 167–186, 1994.

    Google Scholar 

  22. F. Parlamento and A. Policriti. Expressing infinity without foundation. J. Symbolic Logic, 56(4):1230–1235, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  23. L. C. Paulson. Set Theory for verification: I. From foundations to functions. J. Automated Reasoning, 11(3):353–389, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  24. L. C. Paulson. Set Theory for verification. II: Induction and recursion. J. Automated Reasoning, 15(2):167–215, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  25. L. C. Paulson and K. Grabczewski. Mechanizing set theory. J. Automated Reasoning, 17(3):291–323, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  26. A. Quaife. Automated deduction in von Neumann-Bernays-Gödel Set Theory. J. Automated Reasoning, 8(1):91–147, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  27. A. Quaife. Automated development of fundamental mathematical theories. Kluwer Academic Publishers, 1992.

    Google Scholar 

  28. W. V. Quine. Set theory and its logic. The Belknap Press of Harvard University Press, Cambridge, Massachussetts, revised edition, 3rd printing, 1971.

    Google Scholar 

  29. G. Schmidt and T. Ströhlein. Relation algebras: concepts of points and representability. Discrete Mathematics, 54:83–92, 1985.

    Article  MATH  MathSciNet  Google Scholar 

  30. J. R. Shoenfield. Mathematical logic. Addison Wesley, 1967.

    Google Scholar 

  31. A. Tarski. Sur les ensembles fini. Fundamenta Mathematicae, 6:45–95, 1924.

    Google Scholar 

  32. A. Tarski. On the calculus of relations. Journal of Symbolic Logic, 6(3):73–89, 1941.

    Article  MATH  MathSciNet  Google Scholar 

  33. A. Tarski and S. Givant. A formalization of set theory without variables, volume 41 of Colloquium Publications. American Mathematical Society, 1987.

    Google Scholar 

  34. L. Wos. Automated reasoning. 33 basic research problems. Prentice Hall, 1988.

    Google Scholar 

  35. L. Wos. The problem of finding an inference rule for set theory. J. Automated Reasoning, 5(1):93–95, 1989.

    Article  MATH  MathSciNet  Google Scholar 

  36. E. Zermelo. Untersuchungen über die Grundlagen der Mengenlehre I. In From Frege to Gödel-A source book in Mathematical Logic, 1879–1931, pages 199–215. Harvard University Press, 1977.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University “La Sapienza” of Rome, Rome

    Andrea Formisano

  2. Department of Pure and Applied Mathematics, University of L’Aquila, Italy

    Eugenio Omodeo

Authors
  1. Andrea Formisano
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Eugenio Omodeo
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Leibniz-IMAG, 46 Avenue Felix Viallet, 38031, Grenoble cedex, France

    Ricardo Caferra

  2. Technical University of Vienna, Favoritenstraße 9-11/E185-2, 1040, Vienna, Austria

    Gernot Salzer

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Formisano, A., Omodeo, E. (2000). An Equational Re-engineering of Set Theories. In: Caferra, R., Salzer, G. (eds) Automated Deduction in Classical and Non-Classical Logics. FTP 1998. Lecture Notes in Computer Science(), vol 1761. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46508-1_12

Download citation

  • DOI: https://doi.org/10.1007/3-540-46508-1_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67190-9

  • Online ISBN: 978-3-540-46508-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation