An important consequence of the completeness theorem is that it is possible to enumerate the logical consequences of any effective first-order theory, by enumerating all the correct deductions using axioms from the theory.

Gödel’s incompleteness theorem, referring to a different meaning of completeness, shows that if any sufficiently strong effective theory of arithmetic is consistent[,] then there is a formula (depending on the theory) which can neither be proven nor disproven within the theory. Nevertheless the completeness theorem applies to these theories, showing that any logical consequence of such a theory is provable from the theory.

— 14 February 2012

— Wikipedia on Gödel’s completeness theorem

2013.07.19 Friday ACHK