If we consider Gödel’s second incompleteness Theorem i.e. For any formal effectively generated theory T including basic arithmetical truths and also certain truths about formal probability, if T includes a statement of its own consistency then T is inconsistent, we can try to avoid its hypothesis to get results of consistency. The first idea is that the second theorem can apply to Peano arithmetic. So if we want a consistent theory we have to be weaker. The second idea is that even the weak fragment of Robinson arithmetic, is not sufficient for this approach. The first axioms of Robinson arithmetic are:

1. Sx ≠ 0, 2. (Sx = Sy) → x = y 3. y=0 ∨ ∃x (Sx=y), 4. x+0=x, 5. x+Sy=S(x+y), 6. x0=0, 7. xSy=(xy)+x.

So Willard in 2001 introduced a new family of system that are self-verifying theories. Because they are much weaker than Peano arithmetic, even if they are first-order system, they are capable of proving their own consistency. The clue of the idea of Willard, is to avoid the formalization of diagonalisation because he wanted as much as possible elements of the Gödel machinery for the provability aspect but not too much to keep the capacity to prove consistency. For this reason, addition and multiplication we not functions of Willard’ s language. With this methodology each provability of a sentence can be encoded as an arithmetic sentence describing termination of an analytic tableau. Then provability of consistency can be added as an axiom. So the resulting system can be proven consisted.