= Full set of first-order sentences
{title2=$T\vdash\exists x\phi(x)\Longrightarrow\exists t\text{ closed},\ T\vdash\phi(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>.
Back to article page
