2) Can we write a version of this program that would reject at least some spurious proofs?
It's trivial to do at least some:
def A(P):
if P is a valid proof that A(P)==a implies U()==u, and A(P)!=a implies U()<=u
and P does not contain a proof step "A(P)=x" or "A(P)!=x" for any x:
return a
else:
do whatever
Sure, but that's too trivial for my taste :-( You understand the intent of the question, right? It doesn't call for "an answer", it calls for ideas that might lead toward "the answer".
If it's worth saying, but not worth its own post, even in Discussion, it goes here.