  We continue our investigation into hybrid polyadic multi-sorted logic with a
focus on expresivity related to the operational and axiomatic semantics of
rogramming languages, and relations with first-order logic. We identify a
fragment of the full logic, for which we prove sound and complete deduction and
we show that it is powerful enough to represent both the programs and their
semantics in an uniform way. Although weaker than other hybrid systems
previously developed, this system is expected to have better computational
properties. Finally, we provide a standard translation from full hybrid
many-sorted logic to first-order logic.
