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”.
To tell the truth, I just wanted to write something, to generate some activity. The original post seems important and useful, in that it states several well-defined and interesting problems. Seeing it staying alone in a relative obscurity of an Open Thread even for a day was a little disheartening :)
It’s trivial to do at least some:
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”.
To tell the truth, I just wanted to write something, to generate some activity. The original post seems important and useful, in that it states several well-defined and interesting problems. Seeing it staying alone in a relative obscurity of an Open Thread even for a day was a little disheartening :)