gRR comments on An example of self-fulfilling spurious proofs in UDT

gRR 1 Apr 2012 19:37 UTC
0 points
Maybe something like this:
```
def Q():
   return Proof1("IsValidProof(X, Q()) => X") +
          Proof2("IsValidProof(X, Q())") +
          X
```
where IsValidProof(Statement, Proof) is Goedel’s Bew function, Proof1 is a formalization of the argument that “if Q() returns a valid proof of X, then A() will return 1, and X will be true”, and Proof2 is a formalization of the argument that “a valid proof of A=>B, followed by a valid proof of A, followed by B, is a valid proof”.