Let's say a property is an SMT formula.
Let's say a function has a property iff, with addition of the function symbol to a monadic predicate calculus formula over the signature of Presburger arithmetic, that formula is satisfiable. For example, we say that the function $f$ has the property $\forall x, f(x) = x$
Given an arbitrary function symbol $\Phi$, an arbitrary domain $D$, an arbitrary range $R$ such that $$\Phi: D \mapsto R$$ and given a set of properties that the function $\Phi$ has, then is it decidable in the general case to find a definition of the function $\Phi$. In other words, is it decidable to find, in this general case, one property which implies all the others? For example, if you define $f(x) = 2+x$ then the relation $(x, 2+x)$ is a property which would entail all the other properties that $f$ has.
For another example, look back to the above example with function $f$ where $f$ has the property $\forall x, f(x) = x$. This suggests an obvious definition for $f$, but some cases might not be so trivial and I am concerned that this problem is undecidable in its most general setting, but I am not able to prove it to myself.