Andrew_Critch comments on Löb’s Lemma: an easier approach to Löb’s Theorem

[Andrew_Critch]

I’ve now fleshed out the notation section to elaborate on this a bit. Is it better now?

In short, $⊢$ is our symbol for talking about what PA can prove, and $\square$ is shorthand for PA’s symbols for talking about what (a copy of) PA can prove.

• “$⊢$ 1+1=2” means “Peano Arithmetic (PA) can prove that 1+1=2”. No parentheses are needed; the “$⊢$” applies to the whole line that follows it. Also, $⊢$ does not stand for an expression in PA; it’s a symbol we use to talk about what PA can prove.

• “$\square \left(\text{1+1=2}\right)$” basically means the same thing. More precisely, it stands for a numerical expression within PA that can be translated as saying ”$⊢$ 1+1=2″. This translation is possible because of something called a Gödel numbering which allows PA to talk about a (numerically encoded version of) itself.

• ″$\square X$ ” is short for “$\square \left(X\right)$” in cases where “$X$” is just a single character of text.

• “$X⊢Y$” means “PA, along with X as an additional axiom/​assumption, can prove Y”. In this post we don’t have any analogous notation for $\square$.

[quetzal_rainbow]

Thank you, it’s much more clear now.