- Self-verifying theories
Self-verifying theories are consistent first-order systems of
arithmetic much weaker thanPeano arithmetic that are capable of proving their own consistency.Dan Willard was the first to investigate their properties, and he has described a family of such systems. According toGödel's incompleteness theorem , these systems cannot contain the theory of Peano arithmetic, but they can nonetheless contain strong theorems; for instance there are self-verifying systems capable of proving the consistency of Peano arithmetic.In outline, the key to Willard's construction of his system is to formalise enough of the
Gödel machinery to talk aboutprovability internally without being able to formalise diagonalisation. Diagonalisation depends upon not being able to prove multiplication total (and in the earlier versions of the result, addition also). Addition and multiplication are not function symbols of the language; instead, subtraction and division are, with the addition and multiplication predicates being defined in terms of these. Thus, we cannot prove thepi-0-2 sentence expressing totality of multiplication::
With arithmetic expressed in this way provability of a given sentence can be encoded as an arithmetic sentence describing termination of an
analytic tableaux . Provability of consistency can then simply be added as an axiom. The resulting system can be proven consistent by means of arelative consistency argument with respect to regular arithmetic.We can add any valid
Pi-0-1 sentence of arithmetic to the theory and still remain consistent.References
*Solovay, R., 1989. "Injecting Inconsistencies into Models of PA". Annals of Pure and Applied Logic 44(1-2): 101—132.
*Willard, D., 2001. "Self Verifying Axiom Systems, the Incompleteness Theorem and the Tangibility Reflection Principle". Journal of Symbolic Logic 66:536—596.
*Willard, D., 2002. "How to Extend the Semantic Tableaux and Cut-Free Versions of the Second Incompleteness Theorem to Robinson's Arithmetic Q" . Journal of Symbolic Logic 67:465—496.External links
* [http://www.cs.albany.edu/FacultyStaff/profiles/willard.htm Dan Willard's home page] .
Wikimedia Foundation. 2010.