How to progress a database III

In a seminal paper, Lin and Reiter introduced a model-theoretic definition for the progression of a basic action theory in the situation calculus, and proved that it implies the intended properties. They also showed that this definition comes with a strong negative result, namely that for certain cases first-order logic is not expressive enough to correctly characterize the progressed theory and second-order axioms are necessary. However, they also considered an alternative simpler definition according to which the progressed theory is always first-order definable. They conjectured that this alternative definition is incorrect in the sense that the progressed theory is too weak and may sometimes lose information. This conjecture and the status of the definability of progression in first-order logic has remained open since. In this paper we present two significant results about this alternative definition of progression. First, we prove the Lin and Reiter conjecture by presenting a case where the progressed theory indeed does lose information, thus closing a question that has remained open for more than ten years. Second, we prove that the alternative definition is nonetheless correct for reasoning about a large class of sentences, including some that quantify over situations. (C) 2012 Elsevier B.V. All rights reserved.