= Solution
<Soundness> states that <formal derivability> implies <semantic entailment>:
$$
\boxed{\Gamma\vdash_K\phi\quad\Longrightarrow\quad\Gamma\models\phi.}
$$
For <first-order sentences> this means that every <first-order structure> satisfying all assumptions also satisfies every <first-order sentence> formally derived from them. In the <logical formula> version one uses the usual restrictions on generalization from assumptions with <free variables>.
Strong completeness states the converse:
$$
\boxed{\Gamma\models\phi\quad\Longrightarrow\quad\Gamma\vdash_K\phi.}
$$
Equivalently, every syntactically consistent <set> of <first-order sentences> has a <first-order model>. Equality is interpreted as actual identity, and its usual logical <axioms> and substitution rules are part of the standard calculus. Both assertions hold for arbitrary <sets> of assumptions, rather than only <finite sets>.
Back to article page
