It turns out that the problem of deciding whether a predicate is universally valid in an axiomatic system is also undecidable (and, appropriately enough, called

It turns out that the problem of deciding whether a predicate is universally valid in an axiomatic system is also undecidable (and, appropriately enough, called the decision problem). That is to say, declarative systems "corresponding to" general computation are also undecidable. Which isn't really surprising, since logical recurrence is isomorphic to functional recursion. Hence also why the examples I could readily find of program synthesis are decidable problems, like deciding the maximum of two numbers or deciding membership in a list.