Truth-teller sentences in automated proof-checking machine

Let M be an automated proof-cheking machine which works for ZFC.

Let set A be a set of all "well-formed" mathematical logic sentences. For any x∈A, I think M(x) will work in ZFC.

Let sentence m be

m : "a sentence whose Godel number is i is true" and m' is well-formed formula of m.

And we found that the Godel number of m' is i.

(Simply, m' says that "I am true")

What's the result of M(m') ?

-

It's a bit difficult to tell what exactly you're asking, but I hope the following answer helps.

You write:

m : "a sentence whose Godel number is i is true"

(Simply, m' says that "I am true")

This is problematic, since by Tarski's undefinability theorem, there is no way to express the predicate "true" in ZFC (or any other sufficiently complicated formal system). This means that there is no formula $\phi(x)$ in ZFC such that $\phi(A)$ is true if and only if $A$ is a code for a true sentence of ZFC.

But there is a formula $\phi(x)$ is ZFC such that $\phi(A)$ is true if and only if $A$ codes a valid proof of a given sentence of ZFC. This is your automated proof-checking machine. It's important not to confuse "provable" and "true" here.

Now, I'm assuming that this question is motivated by the proof of Gödel's theorem, which involves concocting a sentence of ZFC whose meaning amounts to "This sentence is not provable". It's easy to see that such a sentence can't be proven or disproven if ZFC is consistent. But a natural question is to ask about a similar sentence which can be concocted by the same methods whose meaning amounts to "This sentence is provable." Is such a sentence actually provable, or not?

The answer is that it is provable. This is a consequence of Löb's theorem, which states that if ZFC can prove "If P is provable, then P", then ZFC can prove P. If P is a statement which is equivalent to "P is provable," then one can prove in ZFC that if "P is provable" then P (since this is what P means!) So Löb's theorem applies.

Edited following outside discussion:

First I want to make one point about the set-up here. I used the wording "returns yes if $A$ is a valid proof of a given sentence of ZFC" above, but I'd like to adjust that a little bit.

Our proof checking machine should actually take two inputs, $A$ and $B$. Then: $M(A,B) = 0$ if $A$ codes a valid proof of the sentence coded by $B$ $M(A,B) = 1$ if $A$ does not code a valid proof of the sentence coded by $B$

Yes, we can "physically" build a machine - or write a computer program - which does this. It decodes $A$, then goes through it line by line checking that 1. Each line follows from the previous lines by one of the deduction rules of our system 2. The proof ends with a valid deduction of $B$ Now "$M(A,B) = 0$" means "$A$ is a proof of $B$" and "$M(A,B) = 1$" means "$A$ is not a proof of $B$". $M$ is guaranteed to return $0$ or $1$ on any input.

Notice that this machine $M$ doesn't address the question of whether $B$ is provable. It just answers the question of whether $A$ is a proof of $B$ (Of course if $A$ is a proof of $B$, then $B$ is provable, but if $A$ is not a proof of $B$, we still don't know whether $B$ is provable. It could have some other proof which is not $A$).

Now we can alter our machine a bit to a machine $M'$ which attempts to answer the question "is $B$ provable?", or equivalently "does there exist some $A$ which codes a proof of $B$?" To evaluate $M'(B)$, $M'$ works as follows: it cycles one by one through all the possible codes $A$. For each one, it runs $M(A,B)$. If it gets the answer $0$, then $A$ codes a proof of $B$, so it returns $0$ ("Yes, $B$ is provable!"). If it gets the answer $1$ it moves on to the next code and repeats. Now $M'$ is a very different sort of machine. If $B$ is provable, then $M'$ will eventually find the proof and return $0$. But if $B$ is not provable, $M'$ will keep cycling through all the codes (there are infinitely many of them) forever, looking for a proof. The algorithm will never terminate.

It is this $M'$ that we diagonalize against when we write down sentences like "I am provable" or "I am not provable".

So to answer your specific question, we have a sentence $B$ which means "$M'(B) = 0$" (i.e. $B$ is provable). If you feed $B$ to our machine $M'$, $M'$ will actually terminate and return $0$, that is, it will find us a proof of $B$.

The proof of this, as I said above, is Löb's theorem,

-
Thank you! @Alex Kruckman, You gave me very precise and kind explanation! I appreciate you. I have one more question. I learned that there is no way to express the predicate "true" in ZFC. However, what about this? For the proof-checking machine ϕ, let statement A be : "True if and only if ϕ(A) is true" // Now, what's the result of ϕ(A)? Still undefinable? – HoCheol SHIN Mar 19 '13 at 5:48
You can't express "$A$ is true if and only if $\phi(A)$ is true", because you can't express "$A$ is true". But you can write down a statement $A$ which is equivalent to $\phi(A)$, i.e. it is true if and only if $\phi(A)$ is true. This is the sentence I'm talking about in my answer. – Alex Kruckman Mar 19 '13 at 6:43