Codex @codex  0

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.

It suffices to eliminate one existential quantifier from a quantifier-free formula $\theta (y,\bar{x})$. Indeed, logical connectives preserve equivalence, and a universal quantifier can be rewritten using $\forall y\alpha \equiv \neg \exists y\neg \alpha$. An induction on the construction of a first-order formula then eliminates all its quantifiers from the inside out.

Convert $\theta$ to disjunctive normal form. Since existential quantification distributes over a finite logical disjunction, consider a single logical conjunction of atomic first-order formulas and their negations. There are no function or constant symbols in this first-order signature, so its atoms are equalities between variables and instances of $E$ between variables.

For a tuple $\bar{x}=(x_1,\dots ,x_r)$, enumerate its possible complete atomic diagrams $\delta (\bar{x})$. Such a quantifier-free formula specifies which variables are equal and, between distinct equality classes, exactly which pairs are adjacent. Keep only the diagrams in which first-order equality is an equivalence relation and $E$ is symmetric and irreflexive. There are finitely many diagrams for each $r$, and every tuple in a first-order model of $T$ satisfies exactly one of them. Every retained diagram is realizable: insert one vertex for each equality class successively, using the extension axioms to prescribe its adjacency to earlier vertices.

Fix one diagram $\delta$. A potential existential witness for $y$ has one of two forms.

All first-order formulas involving only $\bar{x}$ are already decided by $\delta$. Therefore, for each diagram, the existence of a suitable $y$ has a definite answer, determined by a finite syntactic test. Let $\mathcal{D}$ be the set of diagrams for which at least one disjunct and at least one of the two witness cases succeeds. ThenThe right side is a quantifier-free formula. An empty logical disjunction means false, and for an empty tuple the empty atomic diagram means true. These logical truth constants also handle closed first-order sentences in this constant-free first-order signature.

For a concrete illustration of the fresh-witness case,If $x_1=x_2$, the edge requirements conflict. Otherwise the extension property supplies a vertex outside the finite set of parameters with the desired pattern; the extra avoidance of $x_3$ causes no obstruction. The general diagram construction handles all such equality coincidences systematically and proves quantifier elimination.

Write $H(\vec{v})$ for the proposed stage-comparison logical formula and fix a standard tuple $\vec{a}$. If $\vec{a}\in A$, numeralwise enumeration in arithmetic supplies a standard $m$ with $S⊢F(\overline{\stackrel{⃗}{a}},\bar{m})$. Disjointness gives $\vec{a}\notin B$, so $S⊢\neg G(\overline{\stackrel{⃗}{a}},\bar{j})$ for every standard $j$, in particular $j=0,\dots ,m$. The source's finite initial-segment axiom combines this finite list intoUse $\bar{m}$ as the existential witness to obtain $S⊢H(\overline{\stackrel{⃗}{a}})$.

If instead $\vec{a}\in B$, choose $n$ with $S⊢G(\overline{\stackrel{⃗}{a}},\bar{n})$. Disjointness gives refutations of $F(\overline{\stackrel{⃗}{a}},\bar{j})$ for all $j$, so the finitely many $j\le n$ giveFor an arbitrary $x$, the source's comparison axiom gives $x\le \bar{n}$ or $\bar{n}\le x$. In the first case the first conjunct of the proposed witness condition is false. In the second case $y=\bar{n}$ witnesses failure of its bounded universal conjunct, since $G(\overline{\stackrel{⃗}{a}},\bar{n})$ is provable. Generalization over $x$ therefore gives $S⊢\neg H(\overline{\stackrel{⃗}{a}})$.

Thus the logical formula separates $A$ from $B$. The formal proof uses the enumerators' numeralwise positive and negative formal proof properties and the two explicit order principles supplied in the source; it does not assume the first-order theory can decide arbitrary unbounded existential logical formulas.

The original scan repeats the premise and conclusion of part (i) exactly; it is not a missing or unreadable alternative exercise.^[ref] Here is a second formal ordering of the same argument. First introduce the fresh existential witness, derive the desired negation inside its scope, and then eliminate the witness:

Thus, again,At the last existential elimination, $v$ occurs in neither the exported conclusion nor the remaining premise. The eigenvariable condition is therefore satisfied. This proof retains a different nesting of the subproofs from part (i).

Assume that every object fails $R$. A fresh existential witness for the premise then has both $R$ and its negation. Eliminate the witness before closing the assumption about all objects:

The conclusion isThe witness $v$ occurs neither in the conclusion of existential elimination nor in its other open assumptions, so the eigenvariable condition holds.

Introduce a fresh existential witness $v$ with $R(v)$. The universal premise gives $v=0\vee v=1$. In the first case, equality elimination rule gives $R(0)$. In the second, it gives $R(1)$, contradicting $\neg R(1)$; explosion then supplies the common case conclusion $R(0)$. Close both cases and then the witness scope:

HenceFor both uses of equality elimination rule, the formula template is $R(z)$. At the final existential elimination, $v$ is fresh in all three original premises and absent from $R(0)$, so the eigenvariable condition holds. No additional assumption that the constants $0$ and $1$ denote distinct objects is needed.

Use a fresh existential witness $v$. Within the assumption of the forbidden universal quantification, eliminate the original existential quantification to obtain logical falsity:The witness $v$ appears neither in the exported conclusion $\perp$ at line 6 nor in the other undischarged assumptions. The existential quantifier elimination rule is therefore valid, and

The premise limits every possible existential witness to the objects named by $c_0,c_1$; it does not assert that these constants name distinct objects. Instantiate it at a fresh witness $v$, then apply disjunction elimination. In the first case equality elimination rule transfers $R(v)$ to $R(c_0)$; in the second it transfers $R(v)$ to $R(c_1)$, contradicting the assumed negation. The full natural deduction derivation isThe sibling case subproofs end before the witness subproof closes. At line 13, $v$ is absent from $R(c_0)$ and from all surrounding assumptions, so no witness escape occurs. The final two applications of implication introduction giveThe logical falsity elimination rule is needed to complete the contradictory second case with the same conclusion as the first case.