This paper presents a general technique for obtaining new results pertaining to the non-finite axiomatizability of behavioural
(pre)congruences over process algebras from old ones. The proposed technique is based on a variation on the classic idea of
reduction mappings. In this setting, such reductions are translations between languages that preserve sound (in)equations
and (in)equational provability over the source language, and reflect families of (in)equations responsible for the non-finite
axiomatizability of the target language. The proposed technique is applied to obtain a number of new non-finite axiomatizability
theorems in process algebra via reduction to Moller’s celebrated non-finite axiomatizability result for CCS. The limitations
of the reduction technique are also studied. In particular, it is shown that prebisimilarity is not finitely based over CCS
with the divergent process Ω, but that this result cannot be proved by a reduction to the non-finite axiomatizability of CCS modulo bisimilarity. This
negative result is the inspiration for the development of a sharpened reduction method that is powerful enough to show that
prebisimilarity is not finitely based over CCS with the divergent process Ω.
The work of Aceto, Ingolfsdottir and Mousavi has been partially supported by the projects “The Equational Logic of Parallel
Processes” (nr. 060013021), “A Unifying Framework for Operational Semantics” (nr. 070030041) and “New Developments in Operational
Semantics” (nr. 080039021) of the Icelandic Research Fund.