So this sounds like this might lead to an undecidable theory but I thought I would give it a try and ask about it after I found nothing on the subject. I am somewhat interested in finding functions which are counter examples to predicates (or solutions to the inverse rather). I would like to restrict the functions to some small class however (possibly even smaller than primitive recursive) so I think there is hope of this working if I restrict them enough.
Has any work been done in this area? Have any tools been written for such things?