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. To meet Wikipedias quality standards, this article or section may require cleanup. ... In logic and mathematics, a formal system consists of two components, a formal language plus a set of inference rules or transformation rules. ... Broadly speaking, a contradiction is an incompatibility between two or more statements, ideas, or actions. ... Proposition is a term used in logic to describe the content of assertions. ...

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. Proof theory, studied as a branch of mathematical logic, represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. ... Hilberts program, formulated by German mathematician David Hilbert in the 1920s, was to formalize all existing theories to a finite, complete set of axioms, and provide a proof that these axioms were consistent. ...

Although consistency can be proved by means of model theory, it is often done in a purely syntactical way, without any need reference to 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. The Cut-elimination theorem is the central result establishing the significance of the sequent calculus. ... In mathematical logic and theoretical computer science, a rewrite system has the normalization property if every term is strongly normalizing; that is, if every sequence of rewrites eventually terminates to a term in normal form. ... The Curry-Howard correspondence is the close relationship between computer programs and mathematical proofs; the correspondence is also known as the Curry-Howard isomorphism, or the formulae-as-types correspondence. ...

Consistency and completeness

The fundamental results relating consistency and completeness were proven by Kurt Gödel: Kurt Gödel (IPA: ) (April 28, 1906 Brno, then Austria-Hungary, now Czech Republic – January 14, 1978 Princeton, New Jersey) was an Austrian logician, mathematician, and philosopher of mathematics One of the most significant logicians of all time, Gödels work has had immense impact upon scientific and philosophical...

• 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: Gödels completeness theorem is an important theorem in mathematical logic which was first proved by Kurt Gödel in 1929. ... First-order predicate calculus or first-order logic (FOL) is a theory in symbolic logic that permits the formulation of quantified statements such as there is at least one X such that. ... A maximal consistent set is a set of formulae belonging to some formal language that satisfy certain constraints: The set is consistent, that is, no formula is both provable and refutable. ... In mathematical logic, Gödels incompleteness theorems are two celebrated theorems about the limitations of formal systems, proved by Kurt Gödel in 1931. ...

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. Presburger arithmetic is the first-order theory of the natural numbers with addition. ... Self-verifying theories are consistent first-order systems of arithmetic much weaker than Peano arithmetic that are capable of proving their own consistency. ...

Formulas

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

Φ is said to be maximally consistent if and only if for every formula φ, if Con then .

Φ is said to contain witnesses if and only if for every formula of the form there exists a term t such that . See First-order logic. It has been suggested that Predicate calculus be merged into this article or section. ...

Basic Results

1. The following are equivalent:

(a) IncΦ

(b) For all

2. Every satisfiable set of formulas is consistent, where a set of formulas Φ is satisfiable if and only if there exists a model such that .

3. For all Φ and φ:

(a) if not , then Con;

(b) if Con Φ and , then Con;

(c) if Con Φ, then Con or Con.

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

(a) if , then ,

(b) either or ,

(c) if and only if or ,

(d) if and , then ,

(e) if and only if there is a term t such that .

Henkin's Theorem

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

Define a binary relation on the set of S-terms if and only if ; and let denote the equivalence class of terms containing ; and let where is the set of terms based on the symbol set .

Define the S-structure over the term-structure corresponding to Φ by:

(1) For n-ary , if and only if ,

(2) For n-ary , ,

(3) For , .

Let be the term interpretation associated with Φ, where .

For all φ, if and only if .

Sketch of Proof

There are several things to verify. First, that 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 is an equivalence relation and also requires a proof that (1) and (2) are independent of the choice of class representatives. Finally, can be verified by induction on formulas. In mathematics, an equivalence relation, denoted by an infix ~, is a binary relation on a set X that is reflexive, symmetric, and transitive. ...

See also

Hilbert's problems

1. Continuum hypothesis
2. Hilbert's third problem
3. Hilbert's fourth problem
4. Hilbert's fifth problem
5. Hilbert's sixth problem
6. Hilbert's seventh problem
7. Riemann hypothesis
8. Hilbert's ninth problem
9. Matiyasevich's theorem
10. Hilbert's eleventh problem
11. Hilbert's twelfth problem
12. Hilbert's thirteenth problem
13. Hilbert's fourteenth problem
14. Hilbert's fifteenth problem
15. Hilbert's sixteenth problem
16. Hilbert's seventeenth problem
17. Hilbert's eighteenth problem
18. Hilbert's nineteenth problem
19. Hilbert's twentieth problem
20. Hilbert's twenty-first problem
21. Hilbert's twenty-second problem
22. Hilbert's twenty-third problem

In mathematics, the continuum hypothesis is a hypothesis about the possible sizes of infinite sets. ... The third on Hilberts list of mathematical problems, presented in 1900, is the easiest one. ... In mathematics, Hilberts fourth problem in the 1900 Hilbert problems was a foundational question in geometry. ... In mathematics, a Lie group (IPA ) is an analytic real or complex manifold that is also a group such that the group operations multiplication and inversion are analytic maps. ... Hilberts sixth problem is to axiomatize those branches of science in which mathematics is prevalent. ... Hilberts seventh problem concerns the irrationality and transcendence of certain numbers (Irrationalität und Transzendenz bestimmter Zahlen). ... Unsolved problems in mathematics: Is the real part of a non-trivial zero of the Riemann zeta function always ½?   In mathematics, the Riemann hypothesis (also called the Riemann zeta-hypothesis), first formulated by Bernhard Riemann in 1859, is one of the most famous unsolved problems. ... In mathematics, Hilberts ninth problem was to find the most general law of reciprocity in an algebraic number field. ... Matiyasevichs theorem, proven in 1970 by Yuri Matiyasevich, implies that Hilberts tenth problem is unsolvable. ... Hilberts eleventh problem, a furthering of the theory of quadratic forms, was stated thus in his landmark speech: It is considered to have been addressed by Helmut Hasses principles in 1923 and 1924. ... Hilberts twelfth problem, of the 23 Hilberts problems, is the extension of Kroneckers Theorem on abelian fields to any algebraic realm of rationality. ... 21. ... Hilberts fourteenth problem asks whether certain subrings are finitely generated. ... Hilberts fifteenth problem is one of the 23 Hilbert problems set out in a celebrated list compiled in 1900 by David Hilbert. ... Hilberts sixteenth problem was posed by David Hilbert at the Paris conference of the International Congress of Mathematicians in 1900, together with the other 22 problems. ... Hilberts seventeenth problem is one of the 23 Hilbert problems set out in a celebrated list compiled in 1900 by David Hilbert. ... Hilberts eighteenth problem is one of the 23 Hilbert problems set out in a celebrated list compiled in 1900 by David Hilbert. ... Hilberts nineteenth problem is one of the 23 Hilbert problems set out in a celebrated list compiled in 1900 by David Hilbert. ... Hilberts twentieth problem is one of the 23 Hilbert problems set out in a celebrated list compiled in 1900 by David Hilbert. ... The twenty-first problem of the 23 Hilbert problems, from the celebrated list put forth in 1900 by David Hilbert, was phrased like this (English translation from 1902). ... Hilberts twenty-second problem is the penultimate entry in the celebrated list of 23 Hilbert problems compiled in 1900 by David Hilbert. ... Hilberts twenty-third problem is one of the last of the 23 Hilbert problems set out in a celebrated list compiled in 1900 by David Hilbert. ...

Reference

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