Abstract: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.