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 such that $T ⊢ X$ and $T ⊢ \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 $□_{P A}$ represents the standard provability predicate in Peano Arithmetic then a sentence of the form $\neg □_{P A} (┌ 0 = 1 ┐)$ represents the consistency of $P A$ , 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 $P A$ .