Your work is wrong. To apply diagonal lemma the definition of phi must be a formula, since you write |- (which is not a formula in PA) I assume you meant it as shorthand for Godels Bew (which is), but you can’t existentially quantify Bew like you did in line 3 of the definition.
Your work is wrong. To apply diagonal lemma the definition of phi must be a formula, since you write |- (which is not a formula in PA) I assume you meant it as shorthand for Godels Bew (which is), but you can’t existentially quantify Bew like you did in line 3 of the definition.
“Your work is wrong” is an unfair characterization of presence of a minor technical inaccuracy.
Yes, I really mean phi to be a formula based on the provability predicate. The third line is really shorthand for
where Sub is a function that replaces the first two free variables in the Gödelized formula with a and b. So we can quantify over a and b.
I suppose I should mention this in the post.