Safety of Formulas in Query Languages, in Set Theory and in Metamathematics

Arnon Avron

We show that there have been common ideas concerning safety properties of formulas which were independently developed in the research on query languages and in the mathematical disciplines of set theory and of metamathematics (of elementary Arithmetics). We introduce a uniform notion of safety of a formula relative to a subset of its set of free variables as a common generalization of the various notions which have been employed in these areas, and show that it is useful for all of them. In the database case the main interest so far has in fact been in safety of a formula relative to the whole set of its free variables. The generalized relative notion provides, however, a firm theoretical foundation for using in queries complex terms, infinite relations, and (most important:) relations that are only partially accessible through links (like in the world wide web). In set theory our notion provides a new understanding and formulation of the axioms of ZF. We show that the various comprehension axioms of this theory (pairing, union, separation axioms, replacement axioms and powerset) can be replaced by the following principle: accept as an axiom any instance of ∃Z(∀x.x ∈ Z ⇔ A) in which A is safe relative to {x}. On the other hand safety relative to the empty set of variables is equivalent to absoluteness. In Arithmetics our notion provides a new understanding of ∑_{0} formulas and of p.r. formulas. In this case the main interest is again in safety relative to the empty set of variables. However, the more general notion not only leads to a neat new definition of these classes, but also to a refined classification of them according to the choice of basic language and the safety properties of its atomic formulas.

Address: Computer Science Department, Tel Aviv University, Tel Aviv, Israel

E-mail: aa@math.tau.ac.il