Gödel's incompleteness theorems are two limitations on axiomatic reasoning. In their usual modern form, they apply to a consistent axiomatic system 
whose axioms form a recursively
enumerable set and which is strong enough to formalize elementary arithmetic.
1. Gödel's first incompleteness theorem states that 
is incomplete: there is a proposition 
such that neither 
nor its negation can be proved
in 
.
2. Gödel's second incompleteness theorem states that if 
is consistent, then, with
the usual arithmetical encoding of proofs, the proposition
formalizing the assertion that 
is consistent has no proof
in 
.
The second incompleteness theorem formalizes within 
part of the proof underlying the
first incompleteness theorem;
it is not merely a restatement. The incompleteness theorems do not contradict Gödel's completeness theorem. That
theorem concerns logical consequence and formal deduction in first-order
logic, whereas the incompleteness theorems concern the deductive limitations
of one fixed sufficiently strong axiomatic system.
