Is there a simple-but-nontrivial example of a concrete quantifier elimination procedure with a concrete theory, especially one that's a standard example of what a constructive argument for quantifier elimination looks like? Also, what does a complete proof of the existence of quantifier elimination look like for the simple theory of the successor operation described in this question?
From what I've read on quantifier elimination, I gather that not every proof that a given theory has it is constructive.
I'm also assuming a) the theory of the successor operation allows quantifier elimination and b) a complete argument that it allows quantifier elimination is reasonably succinct.
What follows is my attempt to understand the material.
The Wikipedia article on quantifier elimination sketches out a way to construct an argument that a particular theory has quantifier elimination, by first considering statements of the form
$$ \exists x \mathop. L_1 \land L_2 \land \cdots \land L_n $$
Where the elements of $L$ are literals, i.e. either atomic formulas headed by a non-logical predicate, equality, or the negation of a positive literal.
From there, disjunctions can be eliminated using the following rule
$$ (\exists x \mathop. (L_1 \land L_2 \land \cdots \land L_n) \lor (K_1 \land K_2 \land \cdots \land K_n)) \\ \text{is equivalent to} \\ (\exists x \mathop. L_1 \land L_2 \land \cdots \land L_n) \,\,\lor\,\, (\exists x \mathop. K_1 \land K_2 \land \cdots \land K_n) $$
The argument for $\forall x \mathop. F$ where $F$ is a quantifier-free formula doesn't make much sense to me.
$$ \forall x \mathop. F \;\; \text{gets sent to} \;\; \lnot \left( \exists x \mathop. \text{negation of $F$ in disjunctive normal form} \right) $$
I think the idea is to eliminate quantifiers in the expression inside the parentheses on the right hand side and then apply negation again to the result, but I'm not sure.
It's also not clear to me why we can't simply strip the $\forall x$ from $F$ directly since free variables are treated identically to universally quantified variables when we're considering which statements are tautologies.
I also read this question, which presents a simple theory with just a successor operation, described below.
It has three axioms $\text{S1}$ through $\text{S3}$ and an axiom schema $\text{S4}$.
$\text{S1}$: Zero has no predescessor.
$$ \forall x \mathop. S(x) \ne 0 \tag{S1} $$
$\text{S2}$: Successor is injective.
$$ \forall x \forall y \mathop. S(x) = S(y) \,\to\, x = y \tag{S2} $$
$\text{S3}$: Every nonzero number has a predecessor.
$$ \forall x \mathop. \left((x \ne 0) \to \left(\exists y \mathop. S(y) = x \right)\right) \tag{S3} $$
$\text{S4}$: The $k$th iterate of successor has no fixed points.
$$ \forall x \mathop. S^k(x) \ne x \tag{Schema S4} $$
The question asks about eliminating quantifiers from sentences of the form $\exists x \mathop. \left( \Delta_1 \land \Delta_2 \land \cdots \land \Delta_n \right)$ where $\Delta$ is a set of positive literals, i.e literals of the form $S^n(x) = S^m(y)$ where $x$ and $y$ are fixed variables.
I suspect that this theory has quantifier elimination as a whole, not just for sentences with existential quantifiers and conjunctions of positive literals.
The answer is somewhat terse, but seems to suggest the following procedure.
Walk each expression in $\Delta$. For every literal $S^n(x) = S^m(y)$, replace $x$ with $S^{(m-n)}(y)$ if $m-n \ge 0$. It doesn't mention explicitly what to do if $n > m$. The answer is also confusing since $x$ can potentially occur in many literals within $\Delta$. I think we just pick one occurrence of $x$ and perform the substitution everywhere in $\Delta_1 \land \Delta_2 \cdots \Delta_n$, but I'm not sure.
It also doesn't mention how to extend the argument to be a full proof of quantifier elimination for the theory of the successor operation, assuming one exists.
This theory does have quantifier elimination, and here's a proof of that fact.
First, here's the definition of a theory having quantifier elimination from Marker's Model Theory: An Introduction.
The important thing to note about this definition is that $\phi \leftrightarrow \psi$ is just another well-formed formula, which means that if a free variable $v$ occurs in $\phi$ and $\psi$ then it appears free in $\phi \leftrightarrow \psi$ overall.
First, let me correct an error in my original question. This theory also has a constant symbol $0$ in addition to the unary function symbol $S$.
In order to prove that a theory has quantifier elimination, it suffices to eliminate quantifiers in expressions of the following form, i.e. a conjunction of literals with a single existentially quantified variable shared between them and arbitrary free variables
$$ \exists x \mathop. L_1 \land \cdots \land L_n $$
For the purposes of this question, let $z$ be a variable that does not occur free in the formula being considered.
Let's proceed by cases
Case 1: $n = 0$
$\exists x \mathop. \top$ is equivalent to $\top$.
Case 2: $n > 0$
First let's define $L^2$ in terms of $L$ as follows.
Every conjunct of $L$ is of the following form, where $p$ and $q$ are variables or $0$.
$$S^j(p) = S^k(q) \;\; \text{or} \;\; S^j(p) \ne S^k(q) $$
Let's consider only the conjuncts where $p$ and $q$ are both $0$.
Note that the truth of $S^j(x) = S^k(x)$ does not depend on the value of $x$ at all, so we can replace it with $S^j(z) = S^k(z)$, and likewise for $\cdots \ne \cdots$.
$$ L^2 \\ \textit{is equal to} \\ \{ l \mathop| l \in L \;\;\text{and $l$ does not have $x$ in both terms} \} \cup \\ \{ S^j(z) = S^k(z) \mathop| \text{$l$ is of the form $S^j(x) = S^k(x)$ and $l \in L$} \} $$
With that out of the way, let's consider three cases. Case 2.1 and 2.2 are split for clarity.
Case 2.1: $L^2$ has no terms containing $x$ at all
If $L^2$ has no terms containing $x$, then the following holds
$$ \exists x \mathop. L_1 \land \cdots \land L_n \;\; \text{is equivalent to} \;\; L^2_1 \land \cdots \land L^2_n $$
Case 2.2: $L^2$ has at least one term with $x$ and $\ne$ but none with $x$ and $=$
If $L^2$ has no terms containing $x$ and $=$, but does have a term containing $x$ and $\ne$, then I claim that the following holds.
$$ \exists x \mathop. L_1 \land \cdots \land L_n \;\; \text{is equivalent to} \;\; \bigwedge \{ l \mathop| l \in L^2 \;\; \text{and $l$ does not contain $x$} \} $$
In order to prove it, note that $\exists x \mathop. L_1 \land \cdots \land L_n$ is true if and only if it holds for all valuations $V$ of the free variables of $L$. Any valuation of $V$ can be extended to include $x$ in the following way. Pick the least element $t$ of $0, S(0), S(S(0)), S^3(0), \cdots$ so that no $L_i$ is false when $x = t$. Every $L_i$ in $L$ either does not contain $x$ or is false for exactly one value of $x$. There are finitely many $L_i$ in $L$ and countably infinitely many elements of the sequence $0, S(0), S(S(0)), S^3(0), \cdots$ so $t$ exists. Therefore, if $\exists x \mathop. L_1 \land \cdots \land L_n$ is true for all valuations then $\bigwedge \{ l \mathop| l \in L^2 \;\; \text{and $l$ does not contain $x$} \}$ is true for all valuations.
If $\bigwedge \{ l \mathop| l \in L^2 \;\; \text{and $l$ does not contain $x$} \}$ is true for all valuations, then adding back the expressions containing $x$ and binding $x$ with an existential quantifier is true for all valuations because only finitely many values of $x$ are ruled out by the new conjuncts.
Case 2.3: $L^2$ has at least one term containing both $x$ and $=$
Here we use the fact that $S$ is an injection in our theory.
Suppose without loss of generality that $L^2_1$ contains $x$ and $=$. Further suppose without loss of generality that $l$ is of the form $S^k(x) = t_2$, i.e. $S^k(x)$ appears on the left rather than the right.
Take every expression from $L^2_2$ through $L^2_n$ and replace apply $S$ $k$ times to both sides, producing $L^3$, with $L^2_1$ unmodified.
$$ L^3_1 = L^2_1 \;\; \text{and} \;\; L^3_{1+n} = \big( L^2_{1+n} \; \text{with $S$ applied $k$ times to both sides} \big) $$
Now note that every occurrence of $x$ occurs inside an expression of the form $S^k(x)$.
Define $L^4$ in the following way, take every occurrence of $S^k(x)$ and replace it with $t_2$.
$$ L^4_i = \big( \text{ $L^3_i$ with $S^k(x)$ replaced with $t_2$ } \big) $$
So the first conjunct in $L^4$ will be $t_2 = t_2$.
$x$ appears nowhere in $L^4$, so
$$ \exists x \mathop. L_1 \land \cdots \land L_n \;\; \text{is equivalent to}\;\; L^4_1 \land \cdots \land L^4_n $$
This completes the argument that the successor theory has quantifier elimination.