Consistency proof

From Wikipedia, the free encyclopedia

In mathematical logic, a formal system is consistent if it does not contain a contradiction, or, more precisely, for no proposition φ are both φ and ¬φ provable.

A consistency proof is a formal proof that a formal system is consistent. The early development of mathematical proof theory was driven by the desire to provide finitary consistency proofs for all of mathematics as part of Hilbert's program. Hilbert's program fell to Gödel's insight that sufficiently strong proof theories cannot prove their own consistency.

Although consistency can be proved by means of model theory, it is often done in a purely syntactical way, without any need to reference some model of the logic. The cut-elimination (or equivalently the normalization of the underlying calculus if there is one) implies the consistency of the calculus: since there is obviously no cut-free proof of falsity, there is no contradiction in general.

Contents

The fundamental results relating consistency and completeness were proven by Kurt Gödel:

By applying these ideas, we see that we can find first-order theories of the following four kinds:

  1. Inconsistent theories, which have no models;
  2. Theories which cannot talk about their own provability relation, such as Tarski's axiomatisation of point and line geometry, and Presburger arithmetic. Since these theories are satisfactorily described by the model we obtain from the completeness theorem, such systems are complete;
  3. Theories which can talk about their own consistency, and which include the negation of the sentence asserting their own consistency. Such theories are complete with respect to the model one obtains from the completeness theorem, but contain as a theorem the derivability of a contradiction, in contradiction to the fact that they are consistent;
  4. Essentially incomplete theories.

In addition, it has recently been discovered that there is a fifth class of theory, the self-verifying theories, which are strong enough to talk about their own provability relation, but are too weak to carry out Gödelian diagonalisation, and so which can consistently prove their own consistency. However as with any theory, a theory proving its own consistency provides us with no interesting information, since inconsistent theories also prove their own consistency.

A set of formulas Φ in first-order logic is consistent (written ConΦ) if and only if there is no formula φ such that \Phi \vdash \phi and \Phi \vdash \lnot\phi. Otherwise Φ is inconsistent and is written IncΦ.

Φ is said to be maximally consistent if and only if for every formula φ, if Con \Phi \cup \phi then \phi \in \Phi.

Φ is said to contain witnesses if and only if for every formula of the form \exists x \phi there exists a term t such that (\exists x \phi \to \phi {t \over x}) \in \Phi. See First-order logic.

1. The following are equivalent:

(a) IncΦ

(b) For all \phi,\; \Phi \vdash \phi.

2. Every satisfiable set of formulas is consistent, where a set of formulas Φ is satisfiable if and only if there exists a model \mathfrak{I} such that \mathfrak{I} \vDash \Phi.

3. For all Φ and φ:

(a) if not \Phi \vdash \phi, then Con\Phi \cup \{\lnot\phi\};

(b) if Con Φ and \Phi \vdash \phi, then Con\Phi \cup \{\phi\};

(c) if Con Φ, then Con\Phi \cup \{\phi\} or Con\Phi \cup \{\lnot \phi\}.

4. Let Φ be a maximally consistent set of formulas and contain witnesses. For all φ and ψ:

(a) if \Phi \vdash \phi, then \phi \in \Phi,

(b) either \phi \in \Phi or \lnot \phi \in \Phi,

(c) (\phi \or \psi) \in \Phi if and only if \phi \in \Phi or \psi \in \Phi,

(d) if (\phi\to\psi) \in \Phi and \phi \in \Phi, then \psi \in \Phi,

(e) \exists x \phi \in \Phi if and only if there is a term t such that \phi{t \over x}\in\Phi.

Let Φ be a maximally consistent set of formulas containing witnesses.

Define a binary relation on the set of S-terms t_0 \sim t_1 \! if and only if \; t_0 = t_1 \in \Phi; and let \overline t \! denote the equivalence class of terms containing t \!; and let T_{\Phi} := \{ \; \overline t \; |\; t \in T^S \} where T^S \! is the set of terms based on the symbol set S \!.

Define the S-structure \mathfrak T_{\Phi} over T_{\Phi} \! the term-structure corresponding to Φ by:

(1) For n-ary R \in S, R^{\mathfrak T_{\Phi}} \overline {t_0} \ldots \overline {t_{n-1}} if and only if \; R t_0 \ldots t_{n-1} \in \Phi,

(2) For n-ary f \in S, f^{\mathfrak T_{\Phi}} (\overline {t_0} \ldots \overline {t_{n-1}}) := \overline {f t_0 \ldots t_{n-1}},

(3) For c \in S, c^{\mathfrak T_{\Phi}}:= \overline c.

Let \mathfrak I_{\Phi} := (\mathfrak T_{\Phi},\beta_{\Phi}) be the term interpretation associated with Φ, where \beta _{\Phi} (x) := \bar x.

(*) \; For all φ,\; \mathfrak I_{\Phi} \vDash \phi if and only if \; \phi \in \Phi.

There are several things to verify. First, that \sim is an equivalence relation. Then, it needs to be verified that (1), (2), and (3) are well defined. This falls out of the fact that \sim is an equivalence relation and also requires a proof that (1) and (2) are independent of the choice of t_0, \ldots ,t_{n-1} class representatives. Finally, \mathfrak I_{\Phi} \vDash \Phi can be verified by induction on formulas.

H.D. Ebbinghaus, J. Flum, W. Thomas, Mathematical Logic

Retrieved from "http://en.wikipedia.org../../../c/o/n/Consistency_proof.html"
Advanced Search
Included Web Search Engines


Safe Search

close

Top Matching Results

Occasionally Search.com will highlight specialized results that are based on the context of your query. Examples of specialized results include specific links to news, images, or video.

Top Matching Results may highlight information from other Search.com pages, content from the CNET Network of sites, or third party content. The listings are based purely on relevance. Search.com does not receive payment for listings in this section but our partners that provide this data may get paid for listing these products.

Sponsored Links

This section contains paid listings which have been purchased by companies that want to have their sites appear for specific search terms and related content. These listings are administered, sorted and maintained by a third party and are not endorsed by Search.com.

Search Results

Search.com sends your search query to several search engines at one time and integrates the results into one list which has been sorted by relevance using Search.com's proprietary algorithm. You can customize the list of search engines included in your metasearch from the preferences.

The search engines that are used in your metasearch may allow companies to pay to have their Web sites included within the results. To view the Paid Inclusion policy for a specific search engine, please visit their Web site. Search.com does not accept payment or share revenue with any search engine partner for listings in this section.