Consistency

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$.