Undecidability confirmed for simple logic with one relation
The Undecidability of FO3 and the Calculus of Relations with Just One Binary Relation
Logic in Computer Science
Summary
Figuring out whether certain simple logical statements are always true is impossible to do with a perfect method. The authors show this problem remains impossible even when using only one kind of relationship between things and limiting the complexity of the logic. They also prove this holds true when looking only at scenarios with a finite number of objects. This means some questions in logic cannot be fully answered even in very simplified settings.
What this means in practice
- •For logic system designers: Know that building decision procedures for FO3 with one binary relation or restricted calculus of relations is impossible due to undecidability limits.
- •For formal verification engineers: Avoid relying on automated validity checking for simplified relational logics, since these problems remain undecidable even with minimal relation complexity.
A theory result. No direct application yet.
Authors
Yoshiki Nakamura
Abstract
The validity problem for first-order logic is a well-known undecidable problem. The undecidability also holds even for $\mathsf{FO}3$ and (equational formulas of) the calculus of relations. In this paper we tighten these undecidability results to the following: (1) $\mathsf{FO}3$ with just one binary relation is undecidable even without equality; and (2) the calculus of relations with just one character and with only composition, union, and complement is undecidable. Additionally we prove that the finite validity problem is also undecidable for the above two classes.