Admissibility of ${\Pi }_2$-Inference Rules: interpolation, model completion, and contact algebras

Abstract

We devise three strategies for recognizing admissibility of non-standard inference rules via interpolation, uniform interpolation, and model completions. We apply our machinery to the case of symmetric implication calculus ${\mathsf{S}}^2\mathsf{IC}$, where we also supply a finite axiomatization of the model completion of its algebraic counterpart, via the equivalent theory of contact algebras. Using this result we obtain a finite basis for admissible ${\Pi }_2$-rules.

25 pages