Abstract
We investigate the decidability of first-order logic extensions. For example, it is established in Zolotov’s works that a logic with a unary transitive closure operator for the one successor theory is decidable. We show that in a similar case, a logic with a unary partial fixed point operator is undecidable. For this purpose, we reduce the halting problem for the counter machine to the problem of truth of the underlying formula. This reduction uses only one unary nonnested partial fixed operator that is applied to a universal or existential formula.
This is a preview of subscription content, log in via an institution to check access.
REFERENCES
A. V. Aho and J. D. Ullman, “Universality of data retrieval languages,” in Proc. 6th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages–POPL ʼ79, San Antonio, Texas, 1979 (Association for Computing Machinery, New York, 1979), pp. 110–119. https://doi.org/10.1145/567752.567763
Yu. Gurevich and S. Shelah, “Fixed-point extensions of first-order logic,” Ann. Pure Appl. Logic 32, 265–280 (1986). https://doi.org/10.1016/0168-0072(86)90055-2
S. M. Dudakov and M. A. Taitslin, “Collapse results for query languages in database theory,” Russ. Math. Surv. 61, 195–253 (2006). https://doi.org/10.1070/rm2006v061n02abeh004311
A. S. Zolotov, “On decidability of the theory with the transitive closure operator,” Lobachevskii J. Math. 36, 434–440 (2015). https://doi.org/10.1134/s1995080215040186
V. S. Sekorin, “On equivalence of PFP-operator and PFP-quantifier,” J. Phys.: Conf. Ser. 1902, 012085 (2020). https://doi.org/10.1088/1742-6596/1902/1/012085
S. M. Dudakov, “On safety of unary and nonunary IFP Operators,” Autom. Control Comput. Sci. 53, 683–688 (2019). https://doi.org/10.3103/s0146411619070034
M. L. Minsky, Computation: Finite and Infinite Machines (Prentice-Hall, Englewood Cliffs, N.J., 1967).
Funding
The work was supported by ongoing institutional funding. No additional grants to carry out or direct this particular research were obtained.
Author information
Authors and Affiliations
Corresponding author
Ethics declarations
The author of this work declares that he has no conflicts of interest.
Additional information
Publisher’s Note.
Allerton Press remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
About this article
Cite this article
Sekorin, V.S. On Undecidability of Unary Nonnested PFP Operators for One Successor Function Theory. Russ Math. 68, 79–82 (2024). https://doi.org/10.3103/S1066369X24700300
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.3103/S1066369X24700300