Equivalence of finite non-deterministic logical matrices is undecidable

TL;DR

This paper demonstrates that determining equivalence between finite non-deterministic logical matrices, which extend traditional propositional semantics, is an undecidable problem, highlighting a fundamental limitation in their use.

Contribution

It proves the undecidability of matrix equivalence in finite non-deterministic logics, revealing a key computational limitation of their expressive power.

Findings

Equivalence problem is undecidable for finite non-deterministic matrices.

Identifies conditions under which equivalence can be effectively checked.

Discusses specific cases and criteria for matrix equivalence.

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.