Solution (source code)

= Solution

The <Godel completeness theorem> for <first-order logic> states that $\Gamma\models\phi$ implies $\Gamma\vdash\phi$; together with soundness, semantic consequence and derivability coincide. Equivalently, every syntactically consistent first-order theory has a model. The <compactness theorem> states that a set of first-order sentences has a model if and only if every finite subset has a model. These statements use nonempty first-order structures.