Editing Self-verifying theories

{{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.

==References==

{{reflist}}

*{{cite journal |last1=Solovay |first1=Robert M. |title=Injecting Inconsistencies into Models of PA |journal=Annals of Pure and Applied Logic |date=9 October 1989 |volume=44 |issue=1–2 |pages=101–132 |doi=10.1016/0168-0072(89)90048-1 |doi-access=free }}
*{{cite journal |last1=Willard |first1=Dan E. |title=Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles |journal=The Journal of Symbolic Logic |date=Jun 2001 |volume=66 |issue=2 |pages=536–596 |doi=10.2307/2695030 |jstor=2695030 |s2cid=2822314 |url=https://www.jstor.org/stable/2695030|url-access=subscription }}
*{{cite journal |last1=Willard |first1=Dan E. |title=How to Extend the Semantic Tableaux and Cut-Free Versions of the Second Incompleteness Theorem almost to Robinson's Arithmetic Q |journal=The Journal of Symbolic Logic |date=Mar 2002 |volume=67 |issue=1 |pages=465–496 |doi=10.2178/jsl/1190150055 |jstor=2695021 |s2cid=8311827 |url=https://www.jstor.org/stable/2695021|url-access=subscription }}

==External links==

* [https://www.albany.edu/ceas/dan-willard.php Dan Willard's home page]. {{Webarchive|url=https://web.archive.org/web/20180818020436/https://www.albany.edu/ceas/dan-willard.php |date=2018-08-18 }}

{{Mathematical logic}}

[[Category:Proof theory]]
[[Category:Theories of deduction]]

{{logic-stub}}