= Types realized in finite structures are principal
Fix a <tuple> in a finite <first-order structure>. For every <tuple> of a different <complete type>, choose a <logical formula> true at the first <tuple> and false at the competitor. The finite <conjunction> selects only <tuples> of the desired <partial type> inside the <first-order structure>. Every implication from that <conjunction> to a member of the <partial type> is true in the <first-order structure> and hence belongs to its <complete theory>. Thus the <conjunction> isolates the <partial type>, even in an infinite <first-order language>.
Back to article page
