Proofs about theorem-provers in ZFC, in ZFC

Question

Is the following statement provable in ZFC for some $A$: "$A$ is an algorithm which, when given as input a proposition $p$ in the language of ZFC, outputs 'yes' only if $p$ is provable in ZFC, 'no' only if $\neg p$ is provable in ZFC, and otherwise does not halt"?

If $A$ enumerates all possible proofs in ZFC until it finds one of $p$ or $\neg p$, then it satisfies the statement. I'm just wondering if there are any issues with expressing the set of provable ZFC propositions within ZFC. My underlying motivation is wondering whether automated-theorem-provers working in an expressive logical system could prove things about correctness and other properties of automated-theorem-provers for the same logical system.

(Apologies if this question is naive or poorly expressed; this is really not my field but I'm trying to understand this concept, so a little extra explanation is greatly appreciated!)

Answer 1

There is no hidden subtlety. The statement in question is indeed provable in ZFC, and it's a good exercise to work through the details.

There is a slight issue, though: it is possible (from the point of view of ZFC at least) that ZFC is inconsistent, and hence that sentences can be proved and disproved. So the following version of your statement is not provable in ZFC (and is, in fact, equivalent - over much less than ZFC - to the consistency of ZFC):

There is an algorithm $A$ such that, on input the Godel number of a sentence $p$, $A$ halts and outputs 1 iff $p$ is provable from ZFC, and halts and outputs 0 iff $\neg p$ is provable from ZFC.

EDIT: This is exactly the issue raised by Henning Makholm's comment, above.

Answer 2

My underlying motivation is wondering whether automated-theorem-provers working in an expressive logical system could prove things about correctness and other properties of automated-theorem-provers for the same logical system.

There are three general issues, at least, with verifying the correctness of the formalized proof predicate within the theory being formalized. We are using ZFC here but essentially any sufficiently strong theory will have the same properties. In the following, Pvbl is the formalized provability predicate.

1. ZFC doesn't prove its own consistency, so ZFC doesn't prove that, for each formula $p$, at most one of Pvbl($p$) and Pvbl($\lnot p$) holds.

2. ZFC might be consistent, but not $\omega$-consistent, and ZFC might actually prove Pvbl($p$) for every $p$. In this case, we can't just add Con(ZFC) as a new axiom, because in this case ZFC + Con(ZFC) would be inconsistent. This point also shows that there are limitations on the ability of ZFC to prove the soundness of its own Pvbl predicate.

3. ZFC is also limited by Löb's theorem. The previous point shows it is possible in principle for Pvbl($p$) and $\lnot p$ to both hold. Löb's theorem shows that if ZFC proves "Pvbl($p$) implies $p$" then ZFC already proves $p$. This shows that there are even more limitations on the ability of ZFC to prove the soundness of its own Pvbl predicate. Moreover, unlike the previous point, Löb's theorem holds even if ZFC is $\omega$-consistent.

Of course, we believe ZFC is $\omega$-consistent, but there are other formal theories of arithmetic that are strong enough to formalize provability but which aren't $\omega$-consistent.