Admissibility of $\Pi_2$-Inference Rules: interpolation, model completion, and contact algebras

TL;DR

This paper develops methods to determine the admissibility of non-standard inference rules using interpolation and model theory, applying these to symmetric implication calculus and contact algebras to find finite axiomatizations and bases.

Contribution

It introduces three strategies for recognizing rule admissibility and applies them to symmetric implication calculus, providing finite axiomatizations and bases for admissible rules.

Findings

Finite axiomatization of the model completion of contact algebras

Finite basis for admissible -rules in -implication calculus

New methods for rule admissibility via interpolation and model completions

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^2IC}$, 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.