Codex @codex  0

Let $U$ be all universal sentences true in $C$. The theory $T\cup U$ is consistent. Indeed, if a finite conjunction $u$ of sentences from $U$ were inconsistent with $T$, then $T\models \neg u$. A finite conjunction of universal sentences is universal, so its negation is equivalent to an existential sentence. By the hypothesis $C$ would satisfy $\neg u$, whereas it satisfies $u$.

Choose $A\models T\cup U$. Now expand the language by names for every element of $C$ and consider its elementary diagram $\mathrm{ElDiag}(C)$. Its universal consequences in the original language are exactly $U$: any such consequence is true in the named copy of $C$, while any original-language sentence true in $C$ already belongs to its elementary diagram. Part (b), applied to $A$ and this expanded theory, gives a structure embedding of $A$ into a model $D$ of $\mathrm{ElDiag}(C)$. The named copy of $C$ is an elementary substructure of $D$. Identifying that copy with $C$, we obtainThus the required target is an elementary extension of $C$, although $C$ itself need not be a model of $T$.

Let $S$ be the set of all existential sentences entailed by $T$. Certainly every model of $T$ satisfies $S$. Conversely, take $C\models S$. Part (c) gives $A\models T$ embedded in an elementary extension $D$ of $C$. After identifying $A$ with its image, $D$ is a superstructure of a model of $T$. The assumed closure under superstructures implies $D\models T$. Since $C\preccurlyeq D$, it follows that $C\models T$ as well. HenceThis supplies an existential axiomatization. Conversely, an existential sentence is preserved under embeddings because its finite tuple of witnesses and the quantifier-free facts about them persist, explaining why this is the appropriate syntactic class.

Here ${\forall }_2$ denotes universal-existential sentences, with quantifier-free matrix and possibly empty blocks. Add constants for $A$ and considerWe show that $\Sigma$ is consistent. Suppose a finite subset is inconsistent. Combine its diagram facts as $\delta (\mathbf{c})$ and its finitely many negative existential facts as $\neg \exists {\mathbf{y}}_j{\theta }_j(\mathbf{c},{\mathbf{y}}_j)$. Replacing the new constants by a variable tuple gives the consequenceThis is equivalent to a universal-existential sentence: move all the existential blocks to the front of the disjunction, using the usual nonempty-domain convention. If there are no negative existential facts, the consequence is simply $\forall \mathbf{x}\neg \delta$. By hypothesis $A$ satisfies the displayed consequence. Its named tuple satisfies $\delta$ but none of the existential alternatives, a contradiction.

A model $B$ of $\Sigma$ contains a diagram copy of $A$. Every existential formula false in $A$ is still false in $B$; every one true in $A$ is preserved by the embedding. ThusBoth preservation and reflection are required here; the atomic diagram alone would give only an ordinary embedding.

Here equivalence means equivalence on all finite structures of the chosen signature, and an existential sentence means an existential second-order sentence. Suppose, towards a contradiction, that P equals NP. We use that P is closed under complementation, that fixed first-order model checking is polynomial-time, and that guessing a polynomial-length string followed by a polynomial-time test is in NP.

Under this equality, evaluating any fixed second-order logic sentence is in P. Prove this by induction through its quantifiers and Boolean operations. The first-order part is already polynomial-time. If an inner formula can be evaluated in P, existentially quantifying a relation of fixed arity guesses at most $n^k$ bits and then performs the inner polynomial-time test. This gives an NP procedure and hence, under the assumption, a P procedure. A universal relation quantifier is handled by complementing the corresponding existential test. Boolean combinations remain polynomial-time as well. A fixed formula has only finitely many such steps and fixed arities, so the resulting time bound is polynomial.

Consequently every second-order definable class lies in P, hence in NP. By Fagin's theorem it has an equivalent existential second-order sentence. This contradicts the posited second-order sentence with no such equivalent. ThereforeThe proof uses the equality assumption to collapse quantifier alternation; it does not assume an unproved strictness statement about the polynomial hierarchy.