Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic.

A non-rigorous way of putting it says that if a formula is logically valid (in first order logic) then there is a formal proof of the formula.

For a proof using the Isabell proof asistant see this pdf

Set Comprehension