arXiv:2610.35770 · v1

The Undecidability of FO3 and the Calculus of Relations with Just One Binary Relation

首次提交 2026-10-27 01:13

版本更新 2026-10-27 01:13

雷达观测 2026-10-29 00:35

摘要

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.

作者备注：Long version of the paper at ICLA'19, with (Ax.1) and (Ax.2) in Section 3 corrected