Safety, Absoluteness, and Computability

Authors Arnon Avron, Shahar Lev, Nissan Levi

Thumbnail PDF


  • Filesize: 445 kB
  • 17 pages

Document Identifiers

Author Details

Arnon Avron
  • School of Computer Science, Tel Aviv University, Tel Aviv, Israel
Shahar Lev
  • School of Computer Science, Tel Aviv University, Tel Aviv, Israel
Nissan Levi
  • School of Computer Science, Tel Aviv University, Tel Aviv, Israel

Cite AsGet BibTex

Arnon Avron, Shahar Lev, and Nissan Levi. Safety, Absoluteness, and Computability. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


The semantic notion of dependent safety is a common generalization of the notion of absoluteness used in set theory and the notion of domain independence used in database theory for characterizing safe queries. This notion has been used in previous works to provide a unified theory of constructions and operations as they are used in different branches of mathematics and computer science, including set theory, computability theory, and database theory. In this paper we provide a complete syntactic characterization of general first-order dependent safety. We also show that this syntactic safety relation can be used for characterizing the set of strictly decidable relations on the natural numbers, as well as for characterizing rudimentary set theory and absoluteness of formulas within it.

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
  • Dependent Safety
  • Computability
  • Absoluteness
  • Decidability
  • Domain Independence


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases. Addison-Wesley, 1995. Google Scholar
  2. H. Andréka, J. van Benthem, and I. Németi. Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic, 27:217-274, 1998. Google Scholar
  3. A. Avron. Constructibility and decidability versus domain independence and absoluteness. Theoretical Computer Science, 394:144-158, 2008. Google Scholar
  4. A. Avron. A framework for formalizing set theories based on the use of static set terms. In A. Avron, N. Dershowitz, and A. Rabinovich, editors, Pillars of Computer Science, volume 4800 of LNCS, pages 87-106. Springer, 2008. Google Scholar
  5. A. Avron. A new approach to predicative set theory. In R. Schindler, editor, Ways of Proof Theory, onto series in mathematical logic, pages 31-63. onto verlag, 2010. Google Scholar
  6. A. Avron and L. Cohen. Formalizing scientifically applicable mathematics in a definitional framework. Journal of Formalized Reasoning, 9(1):53-70, 2016. Google Scholar
  7. A. Avron and L. Cohen. A minimal computational theory of a minimal computational universe. In Proc. of LFCS 2018, pages 37-54, 2018. Google Scholar
  8. D. Cantone, E. Omodeo, and A. Policriti. Set theory for computing: from decision procedures to declarative programming with sets. Springer, 2001. Google Scholar
  9. K. J. Devlin. Constructibility. Perspectives in Mathematical Logic. Springer-Verlag, 1984. Google Scholar
  10. R. A. Di Paola. The recursive unsolvability of the decision problem for the class of definite formulas. J. ACM, 16:324-327, 1969. Google Scholar
  11. S. Feferman. Why a little bit goes a long way: Logical foundations of scientifically applicable mathematics. In PSA: Proceedings of the Biennial Meeting of the Philosophy of Science Association, pages 442-455, 1992. Google Scholar
  12. R. O. Gandy. Set-theoretic functions for elementary syntax. In Axiomatic set theory, Part 2, pages 103-126. AMS, Providence, Rhode Island, 1974. Google Scholar
  13. R. B. Jensen. The fine structure of the constructible hierarchy. Annals of Mathematical Logic, 4:229-308, 1972. Google Scholar
  14. K. Kunen. Set Theory, An Introduction to Independence Proofs. North-Holland, 1980. Google Scholar
  15. A. O. Mendelzon and T. Milo. Formal models of web queries. In Proceedings of the Sixteenth ACM Symposium on Principles of Database Systems, pages 134-143, 1997. Google Scholar
  16. R. Ramakrishnan, F. Bancilhon, and A. Silberschatz. Safety of recursive horn clauses with infinite relations. In ACM SIGACT-SIGMOD Symp. on Principles of Database Systems, San Diego, 1987. Google Scholar
  17. R. M. Smullyan. The Incompleteness Theorems. Oxford University Press, 1992. Google Scholar
  18. R. Topor. Safe database queries with arithmetic relations. In Proceedings of the 14th Australian Computer Science Conference, pages 1-13, Sydney, 1991. Google Scholar
  19. Rodney W. Topor. Domain-independent formulas and databases. Theoretical Computer Science, 52(3):281-306, 1987. Google Scholar
  20. J.D. Ullman. Principles of Database and Knowledge-base Systems. Computer Science Press, 1988. Google Scholar