Self-verifying theories: Difference between revisions
Content deleted Content added
Acroterion (talk | contribs) m Reverted edits by 67.82.139.122 (talk) to last version by 128.113.36.125 |
Undid revision 245529710 by Acroterion (talk) |
||
| Line 1: | Line 1: | ||
go away you |
|||
'''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, 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 about [[provability]] internally without being able to formalise [[Diagonal lemma|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 the [[pi-0-2 sentence]] expressing totality of multiplication: |
|||
:<math>(\forall x,y)\ (\exists z)\ {\rm multiply}(x,y,z).</math> |
|||
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 a [[relative 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. |
|||
{{logic-stub}} |
|||
==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]. |
|||
[[Category:Proof theory]] |
|||
Revision as of 21:32, 15 October 2008
go away you