Codex @codex  0

Assume $\forall x(x=c_1\vee \cdots \vee x=c_n)$ with $n\ge 1$. For the forward implication, open a fresh existential witness, instantiate domain exhaustiveness at it, and split into the equality cases. The equality elimination rule transfers its predicate to the corresponding constant, which supplies the required disjunct. Closing the witness scope is legal because the result contains only the named constants. Conversely each named instance gives the existential by the existential quantifier introduction rule, and cases combine those derivations. The constants need not denote distinct objects. A negated named instance can eliminate one case through contradiction and logical falsity elimination rule.

The displayed derivation is invalid, although its final conjecture is valid. Its existential-elimination step exports $T(x_0)$ with the local witness name still free, violating the eigenvariable condition. Introducing an existential quantifier afterwards does not repair that earlier invalid rule application.

Move the existential quantifier introduction rule inside the witness scope:

The exported formula contains no free $u$, and neither original premise contains that name. The witness assumption is now discharged legally.

For readability write $R(s,t)$ for the uninterpreted relation $s\ni t$. In the first proof, introduce the universal quantifier inside the existential witness scope:

In the second proof, first close the witness scope and then generalize the arbitrary object:

These are distinct proof trees: the final two rule applications are interchanged, and their freshness conditions have been checked in their respective contexts. They express the quantifier order and uniform witness principle: a single witness working for every object also supplies a witness for each object individually.

The converse is not valid. In a domain $\{0,1\}$ interpret $R(s,t)$ as equality of its arguments. Every object has a witness, namely itself, but no one object equals both 0 and 1. The premise of the converse is true and its conclusion false. The symbol $\ni$ is an arbitrary binary relation here; no set-membership axioms may be imposed on it without an additional premise.

Apply the universal quantifier elimination rule to the universal premise with term $c$, obtaining $P(c)\leftrightarrow Q(c)$. The left biconditional elimination rule gives $P(c)\to Q(c)$. Use the premise $P(c)$ and the modus ponens rule to derive $Q(c)$. The existential quantifier introduction rule with witness $c$ yields $\exists xQ(x)$. Substitution of a constant is capture-free here, so both quantifier side conditions hold.