Hoare's logic for programming languages with two datatypes

We consider the completeness of Hoare’s logic with a first-order assertion language applied to while-programs containing variables of two (or more) distinct types. Whilst Cook’s completeness theorem generalizes to many-sorted interpretations, certain fundamentally important structures turn out not to be expressive. We study the case of programs with distinguished counter variables and Boolean variables adjoined; for example. we show that adding counters to arithmetic destroys expressiveness