Codex @codex  0

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.

Let $K$ abbreviate $Q(c_1)\vee Q(c_2)$, and group the three equality alternatives on the left. The proof uses the binary disjunction elimination rule twice, so no unproved three-way derived rule is needed.

The witness name is absent from $K$ and from every assumption remaining after line 19, so the existential elimination is legal. Each equality is used in the forward direction supplied by the printed equality rule. The three named constants need not denote distinct objects: the case proof requires only that they exhaust the domain. This is existential quantification over a finitely named domain followed by exclusion of the first case.

Temporarily assume $Q(c)$ under label $a$. The implication premise and the modus ponens rule yield $\forall x(P(x)\leftrightarrow P(c))$. Instantiate it at $c^{\prime }$ using the universal quantifier elimination rule, obtaining $P(c^{\prime })\leftrightarrow P(c)$. Its right biconditional elimination rule gives $P(c)\to P(c^{\prime })$.

Apply the modus ponens rule with the premise $P(c)$ to obtain $P(c^{\prime })$. Together with $\neg P(c^{\prime })$, negation elimination rule gives $\perp$. Discharge $a$ using the negation introduction rule to conclude $\neg Q(c)$. Nothing assumes that the two constant symbols denote different objects; if they denoted the same object, the stated premises would themselves already be inconsistent.

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.

Let $u$ be fresh, not free in any of the three universal premises. Universal quantifier elimination rule gives $\neg P(u)\vee R(c,u)$, $Q(u)\to R(c,u)$ and $P(u)\vee Q(u)$. Apply disjunction elimination rule to the last formula.

In the $P(u)$ branch, apply disjunction elimination rule to $\neg P(u)\vee R(c,u)$. Its $\neg P(u)$ case contradicts $P(u)$ by negation elimination rule, and logical falsity elimination rule then gives $R(c,u)$. Its $R(c,u)$ case already gives that conclusion. Discharge those two inner case assumptions to obtain $R(c,u)$ under the outer $P(u)$ assumption. In the outer $Q(u)$ branch, the modus ponens rule applied to $Q(u)\to R(c,u)$ gives $R(c,u)$ directly.

Discharge the two outer case assumptions by disjunction elimination rule. The conclusion $R(c,u)$ now depends only on the universal premises, in which $u$ is not free. Universal quantifier introduction rule therefore gives $\forall xR(c,x)$. All case assumptions have been discharged, and the argument requires no classical reductio ad absurdum.