"Looks like a mathjax error?"

Logical systems capture the intuition behind deductive reasoning\. They are composed of axioms and deductive rules that are chained to compose proofs\. Simple logical systems that are used to talk about numbers, such as $~$PA$~$, can be interpreted as talking about many things through encodings, and in particular they can talk about themselves\. There are expressions in logic that capture the concepts involved in deductions\. However, the most important of them, the provability predicate $~$\\square\_{PA}$~$, fails to satisfy some intuitive properties due to the inability of $~$PA$~$ to prove that non standard numbers do not exists\. Löb's theorem says that if $~$PA$~$ cannot prove $~$A$~$, then it can neither prove that from $~$\\square\_{PA}(\\ulcorener A\\urcorner$~$ follows $~$A$~$\. $~$PA$~$ cannot prove its own consistency, in the sense that it cannot prove that the standard predicate is never satisfied by a contradiction\.

Looks like a mathjax error?