Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Unification with Simple Variable Restrictions and Admissibility of $Π_{2}$-rules

Rodrigo Nicolau Almeida, Silvio Ghilardi

TL;DR

This work addresses the admissibility problem for $Π_{2}$-rules in algebraizable logics by reducing it to standard admissibility through left uniform interpolants. It introduces unification with simple variable restrictions (svr-unification) and develops an algebraic perspective via finitely presented algebras, proving that, under natural interpolation and coherence assumptions, svr-unification types mirror standard unification types, enabling decidability transfers for admissibility. A general decision procedure is derived for $Π_{2}$-admissibility, with concrete demonstrations on logics such as $S5$, $GL$, $Grz$, IPC, $LC$, and lax logic, including the nuclear-implicative semilattices case. The results unify interpolation, unification, and admissibility into a common framework and highlight both the potential and limitations of extending to more complex rules or logics lacking uniform interpolation.

Abstract

We develop a method to recognize admissibility of $Π_{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 $Π_{2}$-rules for many logical systems.

Unification with Simple Variable Restrictions and Admissibility of $Π_{2}$-rules

TL;DR

This work addresses the admissibility problem for -rules in algebraizable logics by reducing it to standard admissibility through left uniform interpolants. It introduces unification with simple variable restrictions (svr-unification) and develops an algebraic perspective via finitely presented algebras, proving that, under natural interpolation and coherence assumptions, svr-unification types mirror standard unification types, enabling decidability transfers for admissibility. A general decision procedure is derived for -admissibility, with concrete demonstrations on logics such as , , , IPC, , and lax logic, including the nuclear-implicative semilattices case. The results unify interpolation, unification, and admissibility into a common framework and highlight both the potential and limitations of extending to more complex rules or logics lacking uniform interpolation.

Abstract

We develop a method to recognize admissibility of -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 -rules for many logical systems.
Paper Structure (9 sections, 18 theorems, 28 equations, 6 figures)

This paper contains 9 sections, 18 theorems, 28 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Admissibility of $\Pi_{2}$-rules in Logical Systems
  3. Unification with Simple Variable Restrictions
  4. Algebraic Characterization of $C$-Unification
  5. Interpolation and Finitely Presented Algebras
  6. Finitary svr-Unification Types
  7. Applications
  8. svr-Unification in Nuclear Implicative Semilattices
  9. Conclusions and Further Work

Key Result

lemma 1

Let $\forall\overline{p}\Gamma/^{2}\phi$ be a $\Pi_{2}$-rule and let $C:=\{p_{1},...,p_{n}\}$. Then $\forall\overline{p}\Gamma/^{2}\phi$ is admissible over $\vdash_{S}$ if and only if whenever $\sigma$ is a $C$-invariant substitution and we have $\vdash_{S}\sigma(\Gamma)$, then we have also $\vdash_

Figures (6)

  • Figure 1: Solution to Unification Problem with Simple Variable Restrictions
  • Figure 2:
  • Figure 3: Injections are Transferable
  • Figure 4: Beck-Chevalley Pullback Square
  • Figure 5: Pullback Stability
  • ...and 1 more figures

Theorems & Definitions (44)

  • definition 1
  • definition 2
  • definition 3
  • lemma 1
  • proof
  • definition 4
  • definition 5
  • definition 6
  • theorem 1
  • definition 7
  • ...and 34 more