Unification with Simple Variable Restrictions and Admissibility of $\Pi_{2}$-rules

TL;DR

This paper introduces a method to determine the admissibility of $$-rules by reducing the problem to a specialized unification problem, enabling decidability results for various logical systems.

Contribution

It establishes a connection between admissibility of $$-rules and unification with simple variable restrictions, providing a new approach to decide admissibility.

Findings

Decidability of $$-rule admissibility for many logical systems.

Reduction of admissibility problem to standard unification under certain conditions.

Applicable to logical systems with algebraic semantics and finite approximation of left uniform interpolation.

Abstract

We develop a method to recognize admissibility of $\Pi_{2}$-rules, relating this problem to a specific instance of the unification problem with linear constants restriction, called here "unification with simple variable restriction". It is shown that for logical systems enjoying an appropriate algebraic semantics and a finite approximation of left uniform interpolation, this unification with simple variable restriction can be reduced to standard unification. As a corollary, we obtain the decidability of admissibility of $\Pi_{2}$-rules for many logical systems.