Editing Gödel's completeness theorem (section)

==Consequences==
An important consequence of the completeness theorem is that it is possible to [[enumerable set|recursively enumerate]] the semantic consequences of any [[effectively computable|effective]] first-order theory, by enumerating all the possible formal deductions from the axioms of the theory, and use this to produce an enumeration of their conclusions.

This comes in contrast with the direct meaning of the notion of semantic consequence, that quantifies over all structures in a particular language, which is clearly not a recursive definition.

Also, it makes the concept of "provability", and thus of "theorem", a clear concept that only depends on the chosen system of axioms of the theory, and not on the choice of a proof system.