A Semantic Theory of Abstractions: A Preliminary Report

In this paper we present a semantic theory of abstractions based on viewing abstractions as interpretations between theories. This theory captures important aspects of abstractions not captured in the theory of abstractions presented by Giunchiglia and Walsh. Instead of viewing abstractions as syntactic mappings, we view abstractions as a two step process: the intended domain model is first abstracted and then a set of (abstract) formulas is constructed to capture the abstracted domain model. Viewing and justifying abstractions as model level transformations is both natural and insightful. We provide a precise characterization of the abstract theory that exactly implements the intended abstraction, and show that this theory, while being axiomatizable, is not always finitely axiomatizable. A simple corollary of the latter result disproves a conjecture made by Tenenberg that if a theory is finitely axiomatizable, then predicate abstraction of that theory leads to a finitely axiomatizable theory.