Page "Foundations of mathematics" Paragraph 90

The Completeness theorem establishes an equivalence in first-order logic, between the formal provability of a formula, and its truth in all possible models.

Precisely, for any consistent first-order theory it gives an " explicit construction " of a model described by the theory ; and this model will be countable if the language of the theory is countable.

However this " explicit construction " is not algorithmic.

It is based on an iterative process of completion of the theory, where each step of the iteration consists in adding a formula to the axioms if it keeps the theory consistent ; but this consistency question is only semi-decidable ( an algorithm is available to find any contradiction but if there is none this consistency fact can remain unprovable ).