Editing Self-verifying theories (section)

{{Short description|Systems capable of proving their own consistency}}
'''Self-verifying theories''' are consistent [[first-order logic|first-order]] systems of [[arithmetic]], much weaker than [[Peano arithmetic]], that are capable of proving their own [[consistency proof|consistency]]. [[Dan Willard]] was the first to investigate their properties, and he has described a family of such systems.  According to [[Gödel's incompleteness theorem]], these systems cannot contain the theory of Peano arithmetic nor its weak fragment [[Robinson arithmetic]]; nonetheless, they can contain strong theorems.

In outline, the key to Willard's construction of his system is to formalise enough of the [[Gödel]] machinery to talk about [[Proof theory|provability]] internally without being able to formalise [[Diagonal lemma|diagonalisation]]. Diagonalisation depends upon being able to prove that multiplication is a total function (and in the earlier versions of the result, addition also). Addition and multiplication are not function symbols of Willard's language; instead, subtraction and division are, with the addition and multiplication predicates being defined in terms of these.  Here, one cannot prove the [[arithmetical hierarchy|<math>\Pi^0_2</math> sentence]] expressing totality of multiplication:
<math display=block>(\forall x,y)\ (\exists z)\ {\rm multiply}(x,y,z).</math> 
where <math>{\rm multiply}</math> is the three-place predicate which stands for <math>z/y=x.</math>
When the operations are expressed in this way, provability of a given sentence can be encoded as an arithmetic sentence describing termination of an [[analytic tableau]]. Provability of consistency can then simply be added as an axiom. The resulting system can be proven consistent by means of a [[relative consistency]] argument with respect to ordinary arithmetic.

One can further add any true <math>\Pi^0_1</math> sentence of arithmetic to the theory while still retaining consistency of the theory.