Self-verifying theories

Self-verifying theories

Self-verifying theories are consistent first-order systems of arithmetic much weaker than Peano 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 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 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:

:(forall x,y) (exists z) { m multiply}(x,y,z).

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.

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.

Игры ⚽ Нужна курсовая?

Look at other dictionaries:

  • Self-verification theory — For self testing in electronics, see built in self test Self verification is a social psychological theory that asserts people want to be known and understood by others according to their firmly held beliefs and feelings about themselves, that is …   Wikipedia

  • Barack Obama citizenship conspiracy theories — A billboard questioning the validity of Barack Obama s birth certificate and by extension his eligibility to serve as President of the U. S.[1] The billboard is part of an …   Wikipedia

  • Gödel's incompleteness theorems — In mathematical logic, Gödel s incompleteness theorems, proved by Kurt Gödel in 1931, are two theorems stating inherent limitations of all but the most trivial formal systems for arithmetic of mathematical interest. The theorems are of… …   Wikipedia

  • List of mathematics articles (S) — NOTOC S S duality S matrix S plane S transform S unit S.O.S. Mathematics SA subgroup Saccheri quadrilateral Sacks spiral Sacred geometry Saddle node bifurcation Saddle point Saddle surface Sadleirian Professor of Pure Mathematics Safe prime Safe… …   Wikipedia

  • Proof theory — is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively defined data structures such as plain lists, boxed… …   Wikipedia

  • List of mathematical logic topics — Clicking on related changes shows a list of most recent edits of articles to which this page links. This page links to itself in order that recent changes to this page will also be included in related changes. This is a list of mathematical logic …   Wikipedia

  • Confirmation bias — (also called confirmatory bias or myside bias) is a tendency for people to favor information that confirms their preconceptions or hypotheses regardless of whether the information is true.[Note 1][1] As a result, people gather evidence and recall …   Wikipedia

  • Leibniz: truth, knowledge and metaphysics — Nicholas Jolley Leibniz is in important respects the exception among the great philosophers of the seventeenth century. The major thinkers of the period characteristically proclaim the need to reject the philosophical tradition; in their… …   History of philosophy

  • Resource-based view — The resource based view (RBV) is an economic tool used to determine the strategic resources available to a firm. The fundamental principle of the RBV is that the basis for a competitive advantage of a firm lies primarily in the application of the …   Wikipedia

  • Christian apologetics — Part of a series on Christianity   …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”