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.
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.