Of particular interest is figuring out whether it is possible to write a formula $~$Prv(x)$~$ which is true iff there exists a proof of $~$x$~$ from the axioms and rules of inference of our theory\.

Does x correspond to a *statement* (as used in the previous sentence about expressiveness), or does the formula Prv(x) correspond to a statement?

What's the relationship between a formula and a statement?

## Comments

Jaime Sevilla Molina

"Formula" and "Statement" can be interchanged freely.

Both refer to well-formed strings in the language of interest, in this case the language of arithmetic ($~$\{+,\dot,0,1\}$~$ and the logical symbols).