Let X be the statement “A(Q())==1 implies U()==5, and A(Q())!=1 implies U()<=5”. Let Q be the program that enumerates all proofs trying to find a proof of X, and returns that proof if found. (The definitions of X and Q are mutually quined.) If X is provable at all, then Q will find that proof, and X will become true (by inspection of U and A). That reasoning is formalizable in our proof system, so the statement “if X is provable, then X” is provable. Therefore, by Löb’s theorem, X is provable. So Q will find a proof of X, and A will return 1.
Doesn’t this amount to saying that we’ve got a proof system that can prove false statements, and is therefore unsound?
ETA: I suppose this relies on the fact that “A(Q())!=1 implies U()<=5” can be made true simply by ensuring that A(Q())=1, regardless of what U equals?
Doesn’t this amount to saying that we’ve got a proof system that can prove false statements, and is therefore unsound?
ETA: I suppose this relies on the fact that “A(Q())!=1 implies U()<=5” can be made true simply by ensuring that A(Q())=1, regardless of what U equals?