Here’s another interesting followup question. My implementation of Q relies on enumerating all proofs in order, so running Q requires exponential time. Is there a “Henkin-style” implementation of Q that constructs the self-referential proof quickly and directly, maybe using the steps of Löb’s theorem or something? That’s how I first tried to construct Q after reading your comments, and failed, but it might still be possible.
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”.
Here’s another interesting followup question. My implementation of Q relies on enumerating all proofs in order, so running Q requires exponential time. Is there a “Henkin-style” implementation of Q that constructs the self-referential proof quickly and directly, maybe using the steps of Löb’s theorem or something? That’s how I first tried to construct Q after reading your comments, and failed, but it might still be possible.
Maybe something like this:
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”.