Self-verifying theories

Self-verifying theories are consistent

; nonetheless, they can contain strong theorems.

In outline, the key to Willard's construction of his system is to formalise enough of the

. 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 ${\displaystyle \Pi _{2}^{0}}$ sentence expressing totality of multiplication: where ${\displaystyle {\rm {multiply}}}$ is the three-place predicate which stands for ${\displaystyle z/y=x.}$ When the operations are expressed in this way, provability of a given sentence can be encoded as an arithmetic sentence describing termination of an argument with respect to ordinary arithmetic.

One can further add any true ${\displaystyle \Pi _{1}^{0}}$ sentence of arithmetic to the theory while still retaining consistency of the theory.

References

• Solovay, Robert M. (9 October 1989). "Injecting Inconsistencies into Models of PA". Annals of Pure and Applied Logic. 44 (1–2): 101–132.
  doi:10.1016/0168-0072(89)90048-1
  .
• Willard, Dan E. (Jun 2001). "Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles". The Journal of Symbolic Logic. 66 (2): 536–596.
  S2CID 2822314
  .
• Willard, Dan E. (Mar 2002). "How to Extend the Semantic Tableaux and Cut-Free Versions of the Second Incompleteness Theorem almost to Robinson's Arithmetic Q". The Journal of Symbolic Logic. 67 (1): 465–496.
  S2CID 8311827
  .

External links

• Dan Willard's home page. Archived 2018-08-18 at the Wayback Machine