Model Completeness and Π2 -rules: the case of Contact Algebras

We give a sufficient condition for deciding admissibility of non-standard inference rules inside a modal calculus S with the universal modality. The condition requires the existence of a model completion for the discriminator variety of algebras which are models of S. We apply the condition to the case of symmetric strict implication calculus, i.e., to the modal calculus axiomatizing contact algebras. Such an application requires a characterization of duals of morphisms which are embeddings (in the model-theoretic sense). We supply also an explicit infinite set of axioms for the class of existentially closed contact algebras. The axioms are obtained via a classification of duals of finite minimal extensions of finite contact algebras.