Existential assertions and quantum levels on the tree of the situation calculus

In a seminal paper, Reiter introduced a variant of the situation calculus along with a set of its properties. To the best of our knowledge, one of these properties has remained unproved and ignored despite its relevance to the planning problem and the expressivity of the theories of actions. We state this property in a more general form and provide its proof. Intuitively, whenever a theory of actions entails that there exists a situation satisfying a first order formula (e.g., a goal), at least one such situation must be found within a predetermined distance from the initial situation. This distance is finite and the same in all the models of the theory, since it depends only on the theory and the formula at hand.