Abstract

Each many-sorted theory can be converted to an unsorted theory. But this conversion procedure is not uniquely determined, leading to a dilemma: which unsorted theory captures the content of the corresponding many-sorted theory?