Universal first-order theory

A universal theory can be axiomatized by sentences whose quantifiers are all universal. Such sentences often forbid specified finite configurations.

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.

Quantifier-free logical formulas have the same truth value in a substructure and its ambient first-order structure on tuples from the smaller carrier. First-order term evaluation agrees; atomic relations agree by restriction; Boolean connectives preserve agreement. A universally quantified quantifier-free matrix true on all ambient tuples is therefore true on all substructure tuples.

The universal consequences $T_{\forall }$ of a first-order theory $T$ are all universal first-order sentences entailed by $T$. Their model class is exactly the class of substructures of models of $T$, up to structure embedding. This characterization follows from the diagram embedding criterion for universal theories.

A first-order theory has its class of first-order models closed under substructures of a first-order structure exactly when it is equivalent to its universal consequences $T_{\forall }$. If $A\models T_{\forall }$, then $T\cup \mathrm{Diag}(A)$ is consistent. Otherwise a finite logical conjunction $\delta$ of signed diagram of a structure sentences yields a universal consequence $\forall \mathbf{x}\neg \delta (\mathbf{x})$ false in $A$. The compactness theorem gives a first-order model of $T$ containing an embedded copy of $A$, and closure under substructures of a first-order structure implies $A\models T$. The converse is preservation of universal sentences. The diagram of a structure must include negated as well as positive atomic sentences so that the resulting map is an embedding, not just a homomorphism.

A first-order model class axiomatized by a theory is closed under extensions exactly when it has an existential axiomatization. If $A$ satisfies all existential consequences of $T$, then $T$ is jointly satisfiable with the universal theory of $A$: any finite obstruction would negate a universal conjunction and produce a violated existential consequence. Embed a model of $T$ into a model elementarily equivalent to $A$, apply extension closure, and transfer truth back to $A$.

A universal sentence has the form $\forall \mathbf{x}\psi (\mathbf{x})$ with quantifier-free formula $\psi$, including an empty quantifier block. Its truth passes from a first-order structure to every substructure of a first-order structure: tuples from the smaller domain are also tuples of the larger domain, and quantifier-free truth agrees. Therefore a first-order theory of universal sentences has a first-order model class closed under substructures of a first-order structure.

A universal-existential sentence has a universal block followed by an existential block and a quantifier-free formula. Such axioms are preserved under unions of chains of structures: the universally chosen tuple occurs in one stage, whose existential witnesses remain in the union. An inductive first-order theory has an axiomatization by these sentences.

If failure of a property has a finite witness, one can often axiomatize the property by a universal sentence forbidding each possible finite witness. Compactness supplies finite witnesses when failure is expressed by inconsistency of an associated theory.