# 911truther comments on Formulas of arithmetic that behave like decision agents - Less Wrong

19 03 February 2012 02:58AM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Sort By: Best

You are viewing a single comment's thread.

Comment author: 03 February 2012 03:10:43AM *  4 points [-]

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.

Comment author: 03 February 2012 03:04:38PM 12 points [-]

"Your work is wrong" is an unfair characterization of presence of a minor technical inaccuracy.

Comment author: 03 February 2012 03:40:53AM 8 points [-]

Yes, I really mean phi to be a formula based on the provability predicate. The third line is really shorthand for

$\exists a,b \operatorname{Prv}(\operatorname{Sub}(\ulcorner ... = x ... = y \urcorner,a,b))$

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.