= Solution
A <canonical first-order structure> is generated by its names: every element is the value of a <closed term>. In the function-free setting permitted here, this means every element is the interpretation of a <constant symbol>. Equivalently, the natural map from <closed terms> modulo <logical equality> in the <first-order structure> onto its carrier is surjective. When canonical is defined specifically using constant names, the same definition and all the arguments below apply in this function-free setting.
A <full set of first-order sentences> has the witness property in its own <first-order language>: whenever it proves an <existential sentence> $\exists x\phi(x)$, some <closed term> $t$ satisfies that the <set> proves $\phi(t)$. In a deductively closed <set>, one can equivalently state this using membership of the <first-order sentences>. In the function-free setting the witness <first-order term> is a <constant symbol>. This is the <Henkin witness property>; fullness does not by itself replace the separate requirements of <first-order consistency> and completeness.
Back to article page
