My next attempt :) Below, “PA” means Peano Arithmetic.
def A():
Enumerate proofs (in PA) by length
if found a proof that "A()==a implies U()==u, and A()!=a implies U()<=u"
then return a
def U():
Enumerate proofs in PA+Consistent(PA) by length up to a very large N
if found a proof that "A()==1"
then return (A()==1 ? 5 : 0)
if(A()==2) return 10
return 0
Proposition: A() returns 1 (if PA is consistent). Proof: Let X = “there exist a!=1 and u, such that: A()==a ⇒ U()==u and A()!=a ⇒ U()<=u”. Let S = “there exists u, such that: A()==1 ⇒ U()==u and A()!=1 ⇒ U()<u”. Let T = “A()==1”. Let ProvableU(P) = the provability formula of U (PA+Consistent(PA), with proofs of length < N). Let ProvableA(P) = the provability formula of A (PA). Let “U⊦ P” mean P is a theorem of U’s proof system. Then:
1. U⊦ ProvableU(T) => S // by inspection of U
2. U⊦ S => ~X // by definitions of X and S
3. U⊦ ProvableU(T) => ~X // from the previous two
4. U⊦ ~X => ~ProvableA(X) // by the axiom Consistent(PA)
5. U⊦ ProvableA(ProvableU(T) => S) // by A's inspection of U
6. U⊦ ProvableA(ProvableU(T)) => ProvableA(S) // from the previous
7. U⊦ ProvableU(T) => ProvableA(ProvableU(T))
// because PA is sufficient to model provability in any formal system
8. U⊦ ProvableU(T) => ProvableA(S) and ~ProvableA(X) // from 3, 4, 6, and 7
9. U⊦ ProvableA(S) and ~ProvableA(X) => T // by inspection of A
10. U⊦ ProvableU(T) => T // from the previous two
11. U⊦ T // by Loeb's theorem
Sorry for not noticing your comment earlier. It would be nice to have a way to subscribe to comment threads.
I don’t understand why the definitions of X and S imply that S ⇒ ~X. Does that rely on specific features of your A and U? For example, if we take a different A and U so that A()==2 and U()==0, then X is true for a=2 and u=0, and S is true for u=1.
My next attempt :) Below, “PA” means Peano Arithmetic.
Proposition: A() returns 1 (if PA is consistent).
Proof:
Let X = “there exist a!=1 and u, such that: A()==a ⇒ U()==u and A()!=a ⇒ U()<=u”.
Let S = “there exists u, such that: A()==1 ⇒ U()==u and A()!=1 ⇒ U()<u”.
Let T = “A()==1”.
Let ProvableU(P) = the provability formula of U (PA+Consistent(PA), with proofs of length < N).
Let ProvableA(P) = the provability formula of A (PA).
Let “U⊦ P” mean P is a theorem of U’s proof system.
Then:
QED
Sorry for not noticing your comment earlier. It would be nice to have a way to subscribe to comment threads.
I don’t understand why the definitions of X and S imply that S ⇒ ~X. Does that rely on specific features of your A and U? For example, if we take a different A and U so that A()==2 and U()==0, then X is true for a=2 and u=0, and S is true for u=1.
Use “Subscribe to RSS Feed” on the right.