Undecidability of Unary Unnested PFP-operators for One Successor
Всеслав Станиславович Секорин · 2023
We continue to investigate semantics of the partial fixed point for infinite algebraic structures. We consider the following definition: a partial fixed point operator is true on those tuples those belong to the relation at almost every step. For this operator, we show that the halting problem for a Minsky machine is reducible to the problem of the truth of partial fixed point logic formulas for the one successor function theory. We establish this result in the case when formulas contain no more than one PFP-operator, and this PFP-operator is unary, and its inner formula is universal.