How can the liar paradox be expressed concisely in symbols? In which formal languages?



Formulas for the liar paradox
The [Liar](http://en.wikipedia.org/wiki/Liar_paradox) is the statement "this sentence is false." It is expressible in any language able to perform self-reference and having a truth predicate. Thus, $L$ is a statement equivalent to $\neg T(L)$. 


Goedel proved that the usual formal languages of mathematics, such as the language of arithmetic, are able to perform self-reference in the sense that for any assertion $\varphi(x)$ in the language of arithmetic, there is a sentence $\psi$ such that PA proves $\psi\iff\varphi(\langle\psi\rangle)$, where $\langle\psi\rangle$ denotes the Goedel code of $\psi$. Thus, the sentence $\psi$ asserts that "$\varphi$ holds of me". 


Tarski observed that it follows from this that truth is not definable in arithmetic. Specifically, he proved that there can be no first order formula $T(x)$ such that $\psi\iff T(\langle\psi\rangle)$ holds for every sentence $\psi$. The reason is that the formula $\neg T(x)$ must have a fixed point, and so there will be a sentence $\psi$ for which PA proves $\psi\iff\neg T(\langle\psi\rangle)$, which would contradict the assumed property of T. The sentence $\psi$ is excactly the Liar.


Goedel observed that the concept of "provable", in contrast, is expressible, since a statement is provable (in PA) say, if and only if there is a finite sequence of symbols having the form of a proof. Thus, again by the fixed point lemma, there is a sentence $\psi$ such that PA proves $\psi\iff\neg\text{Prov}(\langle\psi\rangle)$. In other words, $\psi$ asserts "I am not provable". This statement is sufficiently close to the Liar paradox statement that one can fruitfully run the analysis, but instead of a contradiction, what one gets is that $\psi$ is true, but unprovable. This is how Goedel proved the Incompleteness Theorem.


