Equivalence of finite non-deterministic logical matrices is undecidable

TL;DR

The paper investigates whether two finite non-deterministic matrices define the same logic, i.e., the decidability of $Eqv(\mathsf{NMatr})$ is established as false. The approach proves undecidability via a computable reduction from the theorem existence problem $\mathsf{\exists Thm}(\mathsf{NMatr})$, which in turn reduces from the Halting problem $\mathsf{HALT}$ for Minsky counter machines. A central technique is the tilde construction $\widetilde{\mathbb{M}}$ that injects undesignated values as designated ones, enabling connections to unconstrained logics $\mathbb{U}_\Sigma$ and the relevant reductions. The paper also discusses practical sufficient conditions, such as reexpansions, and surveys methods for proving equivalence or non-equivalence in finite Nmatrices, including a bivaluation-based criterion.

Abstract

The notion of a non-deterministic logical matrix (where connectives are interpreted as multi-functions) extends the traditional semantics for propositional logics based on logical matrices (where connectives are interpreted as functions). This extension allows for finitely characterizing a much wider class of logics, and has proven decisive in a myriad of recent compositionality results. In this paper we show that the added expressivity brought by non-determinism also has its drawbacks, and in particular that the problem of determining whether two given finite non-deterministic matrices are equivalent, in the sense that they induce the same logic, becomes undecidable. We also discuss some workable sufficient conditions and particular cases, namely regarding rexpansion homomorphisms and bridges to calculi.