Full set of first-order sentences ($T⊢\exists x\varphi (x)⟹\exists t\text{ closed},T⊢\varphi (t)$)

A full set of first-order sentences has existential witnesses among names in its own first-order language: if it proves an existential sentence, it proves some closed-term instance of the matrix. For a deductively closed set this may be stated by membership of the first-order sentences. In a function-free first-order language the witness is a constant symbol. A first-order consistent complete full first-order theory has a canonical term model.