Existential axiomatization from extension closure (source code)

= Existential axiomatization from extension closure

A <first-order model> class axiomatized by a <first-order theory>[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 <first-order theory>[theory] of $A$: any finite obstruction would negate a universal <conjunction> and produce a violated existential consequence. Embed a <first-order model>[model] of $T$ into a <first-order model>[model] <elementarily equivalent> to $A$, apply extension closure, and transfer truth back to $A$.