CONSISTENCY PROOF


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, as expressed in his two incompleteness theorems, 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
Consistency and completeness
Formulas
Basic Results
Henkin's Theorem
Sketch of Proof
See also
References

Consistency and completeness


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

★ Gödel's completeness theorem shows that any consistent first-order theory is complete with respect to a maximal consistent set of formulae which are generated by means of a proof search algorithm.

★ Gödel's incompleteness theorems show that theories capable of expressing their own provability relation and of carrying out a diagonal argument are capable of proving their own consistency only if they are inconsistent. Such theories, if consistent, are known as ''essentially incomplete theories''.
By applying these ideas, we see that we can find first-order theories of the following four kinds:
#Inconsistent theories, which have no models;
#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;
#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;
#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.

Formulas


A set of formulas Phi in first-order logic is 'consistent' (written ConPhi) if and only if there is no formula phi such that Phi dash phi and Phi dash lnotphi. Otherwise Phi is 'inconsistent' and is written IncPhi.
Phi is said to be 'simply consistent' iff for no formula phi of Phi are both phi and the negation of phi theorems of Phi.
Phi is said to be 'absolutely consistent' or 'Post consistent' iff at least one formula of Phi is not a theorem of Phi.
Phi is said to be 'maximally consistent' if and only if for every formula phi, if Con Phi cup phi then phi in Phi.
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 o phi {t over x}) in Phi. See First-order logic.
Basic Results

'1.' The following are equivalent:
(a) IncPhi
(b) For all phi,; Phi dash phi.
'2.' Every satisfiable set of formulas is consistent, where a set of formulas Phi is satisfiable if and only if there exists a model mathfrak{I} such that mathfrak{I} Dash Phi .
'3.' For all Phi and phi:
(a) if not Phi dash phi, then Con Phi cup {lnotphi};
(b) if Con Phi and Phi dash phi, then Con Phi cup {phi};
(c) if Con Phi, then Con Phi cup {phi} or Con Phi cup {lnot phi}.
'4.' Let Phi be a maximally consistent set of formulas and contain witnesses. For all phi and psi :
(a) if Phi dash 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 opsi) 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}inPhi.
Henkin's Theorem

Let Phi 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 Phi 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},eta_{Phi}) be the 'term interpretation' associated with Phi, where eta _{Phi} (x) := ar x.

(
★ ) ; For all phi,; mathfrak I_{Phi} Dash phi if and only if ; phi in Phi.

Sketch of Proof

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} Dash Phi can be verified by induction on formulas.

See also



★ Equiconsistency

★ Hilbert's second problem

★ Hilbert's program

★ Hilbert's problems

★ Matiyasevich's theorem

★ Emil Post (1920)

★ Åukasiewicz

References


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

This article provided by Wikipedia. To edit the contents of this article, click here for original source.

psst.. try this: add to faves
©2009 TripAtlas.com