Codex @codex  0

Assume $T$ has quantifier elimination, and let $j:\mathcal{M}\to \mathcal{N}$ be a structure embedding between its models. For any first-order formula $\phi (\bar{x})$, choose a quantifier-free formula $\psi$ equivalent to it modulo $T$. A structure embedding preserves and reflects atomic formulas; induction through the Boolean connectives therefore preserves every quantifier-free formula. ThusThe embedding is elementary. Every theory with quantifier elimination is model-complete.

Use the Gödel-Gentzen negative translation, writing $A^N$ for the translated first-order formula. On atomic formulas $P$, including logical equality, put $P^N=\neg \neg P$, and put ${\perp }^N=\perp$. Extend recursively byLogical negation abbreviates logical implication to logical falsity, so $(\neg A{)}^N=\neg A^N$. The displayed logical disjunction and existential clauses are intuitionistically equivalent to the usual negative clauses $\neg (\neg A^N\wedge \neg B^N)$ and $\neg \forall x\neg A^N$, respectively. Thus these clauses specify the same negative interpretation. Translation commutes with capture-avoiding substitution of terms for free variables.

First prove by structural induction the stability of a formula under double negation:Every double logical negation is stable, since intuitionistic first-order logic proves $\neg \neg \neg \neg C\to \neg \neg C$; logical falsity is stable as well. Stability passes to logical conjunction by obtaining double logical negation of each component. For a logical implication $C\to D$ with stable $D$, assume $\neg \neg (C\to D)$ and $C$. An assumption $\neg D$ would give $\neg (C\to D)$, a contradiction, so $\neg \neg D$ and then $D$. For a universal first-order formula, $\neg \neg \forall xC(x)$ implies $\neg \neg C(y)$ for arbitrary fresh $y$; use stability pointwise and generalize. Logical disjunction and existential translations are already double negations. This proves all cases.

Now regard classical first-order natural deduction as intuitionistic natural deduction plus unrestricted double-negation elimination, and induct on a classical derivation. The rules for logical conjunction, logical implication, universal quantification and logical falsity translate directly. Logical disjunction introduction gives $A^N\vee B^N$ and then its double logical negation. For logical disjunction elimination, the translated premise is $\neg \neg (A^N\vee B^N)$ and the two translated branches yield the stable conclusion $C^N$. Assuming $\neg C^N$ makes each branch contradictory, giving $\neg A^N$ and $\neg B^N$, hence $\neg (A^N\vee B^N)$, which contradicts the premise. We have $\neg \neg C^N$ and remove it by stability.

Existential introduction likewise adds a double logical negation to the ordinary witness introduction. In existential elimination, the witness branch $A^N(y)⊢C^N$ has the original fresh-variable condition. Assuming $\neg C^N$ makes that branch give $\neg A^N(y)$; generalization gives $\forall y\neg A^N(y)$ and therefore $\neg \exists y{A}^N(y)$, contradicting the translated premise. Again stability supplies $C^N$. The universal-rule side conditions are preserved because the translation introduces no new free variables.

For logical equality, reflexivity gives $t=t$ and then its double logical negation. For substitution, from $\neg \neg (s=t)$ and $A^N(s)$, temporarily assume $\neg A^N(t)$. An assumption $s=t$ would transport $A^N(s)$ to $A^N(t)$ by intuitionistic logical equality substitution, so it gives a contradiction and hence $\neg (s=t)$. The first premise contradicts this. Thus $\neg \neg A^N(t)$ holds and stability gives $A^N(t)$. Finally a classical double-negation elimination step translates precisely to $\neg \neg A^N\to A^N$, already proved. Every rule is therefore covered, giving negative translation of a classical proof:In particular a classical thesis has an intuitionistic, constructive translated proof. If nonlogical assumptions are present, they must be translated too.

In classical logic, double-negation elimination gives $P^N\leftrightarrow P$ on atoms. Structural induction propagates equivalence through logical conjunction, logical implication and both quantifiers, and removes the added double negations on logical disjunction and existence. Therefore

A sufficient condition is that $T$ be first-order consistent, complete, and full in its own first-order language. Work in the allowed function-free setting. Since $T$ proves the logically valid first-order sentence $\exists x(x=x)$, fullness guarantees at least one constant and a nonempty collection of names.

Form the carrier from equivalence classes $[c]$ of constant symbols underLogical equality logic makes this an equivalence relation. Interpret a constant by its class and interpret each relation symbol bySubstitution of equals makes this independent of representatives. This defines a canonical first-order structure because every carrier element is named by a constant.

The truth lemma, proved by induction on logical formulas with constants substituted for their free variables, saysAtomic formulas hold by construction; completeness and first-order consistency give the Boolean steps. For the existential step, a witness in the first-order structure is a named class, so its truth gives a proved instance and hence a proved existential sentence. Conversely a proved existential sentence has a constant witness by fullness, and the induction hypothesis realizes that instance in the first-order structure. The universal case follows by negation. Thus $\mathcal{M}\models T$, provingThe witness condition is needed in the original first-order language; adding new constants produces a canonical first-order structure in an expanded first-order language, which is a different assertion.

Use the first-order language with one equivalence relation $E$. Let $\mathcal{A}$ have exactly two equivalence classes, one countably infinite and one uncountable, with no further first-order structure. Its complete theory says that there are exactly two classes and both are infinite.

This first-order theory has quantifier elimination. To eliminate one existential logical variable from a conjunction of atomic formulas and negated atomic formulas, a logical equality either fixes its value, or finitely many inequalities exclude finitely many points. Its required equivalence-class membership is determined by the finitely many existing classes represented among the parameters. A required unused class exists exactly when fewer than two classes have already been used. Once its class is possible, infinitude supplies a point avoiding the finite exclusions. These tests are quantifier-free logical equality and equivalence conditions on the parameters. Disjunctive normal form and induction eliminate all quantifiers and also show completeness.

Thus a finite tuple's complete type is isolated by its finite equality-and-equivalence pattern. Every realized finite-tuple partial type is principal, so $\mathcal{A}$ is atomic. In particular all individual elements have the same complete one-type, isolated by $x=x$.

Choose $a$ in the countable class and $b$ in the uncountable class. Any automorphism taking $a$ to $b$ would give a bijection from their whole equivalence classes, impossible because their cardinalities differ. ThereforeIts uncountability is precisely what avoids the conclusion of (iii).

Here $\mathcal{B}\subseteq \mathcal{A}$ means a substructure, so the smaller carrier contains all named constants, is closed under every function symbol, and has each relation restricted from the larger first-order structure. First-order term evaluation on tuples from $B$ agrees in the two first-order structures. Consequently atomic formulas agree, and induction on Boolean connectives makes every quantifier-free formula agree as well.

Write an arbitrary universal sentence of $T$ as $\forall \vec{x}\theta (\vec{x})$ with quantifier-free matrix. Every tuple from $B$ is also a tuple from $A$, so $\theta$ holds at that tuple in $\mathcal{A}$. Quantifier-free agreement transfers it to $\mathcal{B}$. Since the tuple was arbitrary, $\mathcal{B}$ satisfies the universal sentence. ThusAn arbitrary subset without the substructure operations and relation restrictions would not be the hypothesis used by this formal proof.

For a structure in a countable language and any subset $C$ of its domain, there is an elementary substructure containing $C$ of cardinality at most $\max (|C|,{\aleph }_0)$. In particular a finite or countable $C$ lies in a countable elementary substructure. This is the downward Löwenheim-Skolem theorem.

Construct it directly inside the given structure $A$. Start with $C_0$ containing $C$, the interpretations of the constants, and one element if needed to ensure a nonempty domain. Given $C_n$, for every formula $\exists x\phi (x,a)$ with its finite parameter tuple from $C_n$ that is true in $A$, choose one actual witness in $A$ and place it in $C_{n+1}$. Retain $C_n$ as well. There are at most $\max (|C|,{\aleph }_0)$ choices at each stage. Let $B={\bigcup }_{n<\omega }{C}_n$.

The construction closes $B$ under every function of the language: for a tuple in $C_n$, the formula $x=f(a)$ forces its unique value into the next stage. Thus $B$ carries the induced substructure, and it has the asserted cardinal bound.

Prove elementarity by structural induction. Atomic formulas agree by the induced-substructure construction; logical connectives preserve agreement. For an existential formula with parameters in $B$, if it is true in $A$, all its parameters occur in some $C_n$, so the chosen witness lies in $C_{n+1}\subseteq B$. The induction hypothesis makes its matrix true in $B$. In the other direction a witness in $B$ is also a witness in $A$, again by induction. This is the Tarski-Vaught test, with its witness argument proved explicitly. No completeness or compactness theorem theorem enters the construction.

For the additive zero singleton, $x+x=x$ is already a quantifier-free formula, so it is also an existential formula and a universal formula with an empty quantifier block. If a nonempty block is required, add a dummy $\exists y$ or $\forall y$; first-order domains are nonempty.

For the two definable multiplicative singletons, existential formulas areIn the integers, the equation $x^2=x$ restricts $x$ to zero or one. In the first line, one never satisfies the inequality, whereas zero does with $y=1$. In the second, zero never satisfies it, whereas one does with $y=0$. The respective universal formulas are $\forall y(xy=x)$ and $\forall y(xy=y)$, as already verified.

Neither multiplicative singleton has a quantifier-free formula. In this constant-free, multiplication-only language, every term in the sole free variable $x$ is $x^k$ for a positive integer $k$. Every atomic formula $x^r=x^s$ is true at both zero and one. Every Boolean combination consequently has the same truth value at those two points, and cannot separate their singletons. This is the fact that zero and one have the same quantifier-free type in the multiplicative integers.

Thus additive zero admits all three forms; multiplicative zero and one admit existential and universal forms, but no quantifier-free form. All remaining cases were excluded from definability itself by structure automorphisms.

A structure embedding preserves and reflects all atomic formulas, hence all quantifier-free formulas by induction on Boolean combinations. If $T$ has quantifier elimination, replace any $\phi (\mathbf{x})$ by a quantifier-free $\theta (\mathbf{x})$ equivalent over $T$. For $\mathcal{A}\subseteq \mathcal{B}\models T$ and a tuple $\mathbf{a}$ from $A$,Thus $\mathcal{A}⪯\mathcal{B}$, and the preceding criterion proves $\boxed{\text{quantifier elimination implies model completeness}.}$

The printed expression has one unmatched closing parenthesis. Remove that final surplus parenthesis and read the first disjunct as $\exists xP(x)$; the other disjunct has outer universal quantification over the displayed implication. To distinguish the two independent bound uses of $x$, rename the first to $u$.

Push the outer negation through the logical disjunction and through the quantifiers. Negating the implication preserves its existential antecedent and negates its consequent. Applying De Morgan's laws and the quantifier negation rules gives the negation normal formEach negation is now directly before an atomic formula. No bound variable has been captured, and no original existential quantification in the antecedent has accidentally been negated twice.

Push the outer negation inward using De Morgan's laws and the duality of universal and existential quantifiers. Negating the outer universal quantifier first gives an existential $x$. Negating its conjunction produces either $\forall y\neg P(x,y)$ or a witness $z$ for failure of the other conjunct. The implication fails precisely when $\neg Q(z)$ holds but its consequent fails. Therefore a negation normal form isAll negations now apply directly to atomic formulas. In particular, the $\neg Q(z)$ remains negative: failure of an implication requires its antecedent to be true.

A predicate symbol of arity $k$ is interpreted as a subset of the $k$th Cartesian power of a structure's domain. Applying it to $k$ first-order terms gives an atomic formula. In a singleton domain there is only one possible argument tuple at each arity, but a predicate may still be interpreted as either the empty relation or the full relation.

A primitive positive formula is generated from atomic formulas using only logical conjunction and existential quantification. It can be put in the form $\exists \bar{y}{\bigwedge }_j{\theta }_j(\bar{x},\bar{y})$ with each ${\theta }_j$ atomic. The exam terminology tame formula refers to this fragment. Its reduced product transfer needs only filter intersection and upward closure, together with coordinatewise choices of witnesses.

A quantifier-free first-order formula is built from atomic formulas using logical connectives, with no quantifiers. An embedding of first-order structures preserves and reflects its truth, by mathematical induction on the first-order formula. Both positive and negated atomic information are needed for this conclusion in a relational language.

A recursive presentation identifies the domain of a countable structure with a computable set, with its basic operations given by total computable functions and its basic relations decidable. In a fixed finite signature this makes evaluation of atomic formulas effective. A countable structure may have a recursive presentation of a structure only for some choices of presentation, or none at all.

A structure embedding is an injective map respecting constants and operations and preserving and reflecting relations. Equivalently it preserves all atomic formulas and their negations. It identifies the source with a substructure of the target. An elementary embedding additionally preserves every first-order formula.

A first-order structure and an assignment determine the value of every term recursively: a variable has its assigned value, a constant has its interpreted value, and a compound function term is evaluated by applying the interpreted function to the recursively evaluated arguments. This operation supplies the input values for the satisfaction clauses of atomic formulas.

A function-free implication between conjunctions of positive atomic formulas, allowing existentially quantified witnesses in its conclusion. Standard tuple-generating dependencies do not have disjunctive heads or negative constraints.

Unification finds a substitution making given first-order terms syntactically identical. In first-order unification, a substitution replaces variables by first-order terms while leaving function symbols fixed. A most general unifier captures the necessary identifications: every other unifier follows by a further substitution.^[ref]

For example, $f(x,g(y))$ and $f(g(z),g(a))$ have most general unifier $\{x\mapsto g(z),y\mapsto a\}$. The variable $z$ remains free; assigning it a particular first-order term gives a more specific unifier. Requiring $f(x,x)=f(a,b)$ forces both $x=a$ and $x=b$, so distinct constant symbols $a,b$ make it impossible.

Syntactic identity is essential. With addition treated as a binary function symbol, the first-order terms $x+0$ and $x$ are different even though their values agree under ordinary arithmetic. Equational unification incorporates specified identities and is a different problem. For finite first-order terms, the occurs check rejects $x=f(x)$: a finite first-order term cannot equal one of its proper subterms. Unification makes resolution possible by aligning atomic formulas before inference.

A unifier of first-order terms $s,t$ is a first-order substitution $\sigma$ for which $s\sigma =t\sigma$. The first-order substitution replaces variables by first-order terms; it does not alter function symbols. For example, $\{x\mapsto a,y\mapsto b\}$ unifies $f(x,g(y))$ with $f(a,g(b))$.

A most general unifier leaves every identification not forced by the original equations available for later choice. For $f(x,y)=f(y,z)$, one solution is $\{x\mapsto z,y\mapsto z\}$. The remaining variable $z$ is free. Replacing it by any finite first-order term gives a more specific unifier; arbitrarily choosing $z=a$ during the initial computation would discard that generality.

Not every pair is unifiable. Distinct constant symbols cannot be made equal by replacing variables, and the occurs check rejects $x=f(x)$ for finite first-order terms. These are structural restrictions, not numerical inequalities. Unifiers allow a resolution step to align the relevant atomic formulas before the logical inference is performed.^[ref]

In the constant-free language with multiplication as its sole nonlogical symbol, every term in one free variable is $x^k$ for some $k\ge 1$. Every atomic formula $x^r=x^s$ holds at both zero and one. Hence every quantifier-free formula, being a finite Boolean combination of those atoms, has the same truth value at both points. They have the same quantifier-free type, and neither singleton is quantifier-free definable. Quantifiers distinguish them: $\forall y(xy=x)$ defines zero, while $\forall y(xy=y)$ defines one. These formulas do not rely on named zero or one constants.