= Herbrand disjunction for a universal theory
{c}
{title2=$T\models\exists\vec x\,\theta(\vec x)\Longrightarrow T\models\bigvee_{i=1}^m\theta(\vec t_i)$}
If a universal <first-order theory> in a <first-order language> with a constant entails an <existential sentence> with quantifier-free matrix, it entails a finite disjunction of closed-term instances of that matrix. Otherwise a <first-order model> of the <first-order theory> and all negated ground instances would have a <ground-term substructure> satisfying the <first-order theory>. An <existential witness> there is a <tuple> of closed-term values, contradicting its negated ground instance. <Compactness theorem> extracts finitely many instances.
Back to article page
