I thought it couldn’t find any other proofs of length < N, because it would imply there was no proof of S. But this is not a problem if S is false… Ok, modification:
def U():
Enumerate proofs by length up to a very large N
if found a proof that "A()==1 implies U()==5, and A()!=1 implies U()<=5"
then if(A()==1) return 5
if found any other proof of the same form
then whatever A() return 0
if(A()==2) return 10
return 0
EDIT: Wait, this is not good, now if(A()==2) is unreachable... EDIT2: No, not actually unreachable, but any proof for a statement of the form “A()==2 ⇒ U()==10...” must be of length > N, which is what was needed, I suppose. Still feels like cheating, but I’m not sure why...
I thought it couldn’t find any other proofs of length < N, because it would imply there was no proof of S. But this is not a problem if S is false… Ok, modification:
EDIT: Wait, this is not good, now if(A()==2) is unreachable...
EDIT2: No, not actually unreachable, but any proof for a statement of the form “A()==2 ⇒ U()==10...” must be of length > N, which is what was needed, I suppose. Still feels like cheating, but I’m not sure why...
What’s the intended consequence of A()==2 in your implementation of U? Is it U()==0 or U()==10? And which of those would actually happen?