by Jaime Sevilla Molina Jul 24 2016

A consistent [-theory] is one in which there are well-formed statements that you cannot prove from its axioms; or equivalently, that there is no $~$X$~$ such that $~$T\vdash X$~$ and $~$T\vdash \neg X$~$.

From the point of view of [-model_theory], a consistent theory is one whose axioms are [-satisfiable]. Thus, to prove that a set of axioms is consistent you can resort to constructing a model using a formal system whose consistency you trust (normally using [set_theory]) in which all the axioms come true.

Arithmetic is [ expressive enough] to talk about consistency within itself. If $~$\square_{PA}$~$ represents the Standard provability predicate in Peano Arithmetic then a sentence of the form $~$\neg\square_{PA}(\ulcorner 0=1\urcorner)$~$ represents the consistency of $~$PA$~$, since it comes to say that there exists a disprovable sentence for which there is no proof. [ Gödel's second incompleteness theorem] comes to say that such a sentence is not provable from the axioms of $~$PA$~$.