求基于指定公理的∃v₁∀v₂¬f(v₂)=v₁⊢∃v₁∃v₂¬v₂=v₁推导

咱们用给定的等式公理（E1-E3）加上一阶逻辑的标准量词推理规则来完成这个推导，一步步来：

1. $\exists v_1 \forall v_2 \neg f(v_2)=v_1$
   前提，也就是我们要从它出发推导的初始式子

2. $\forall v_2 \neg f(v_2)=c$
   存在消去规则（EI）：从步骤1引入一个全新的常量$c$（$c$不会在前提或后续推导的其他式子中出现），原前提保证存在这样的$v_1$，咱们就用$c$来指代这个特定的对象

3. $\neg f(c)=c$
   全称消去规则（UI）：对步骤2的全称量词做实例化，用$c$代入$v_2$——既然全称量词对所有$v_2$都成立，那对$c$这个具体对象自然也成立

4. $\exists v_2 \neg v_2=c$
   存在引入规则（EG）：从步骤3出发，把$f(c)$替换成受存在量词约束的$v_2$，既然$\neg f(c)=c$是成立的，那就说明存在某个$v_2$（就是$f(c)$）满足$\neg v_2=c$

5. $\exists v_1 \exists v_2 \neg v_2=v_1$
   存在引入规则（EG）：再把步骤4里的$c$替换成受存在量词约束的$v_1$，这样就得到了我们最终要推导的目标式子

额外补充：这次推导里没用到E2和E3，因为不需要对函数或关系的参数做等式替换；E1的自反性也没直接用到，核心就是量词规则的合规应用——所有实例化和引入的项都符合“可代入”要求，没有出现变量捕获的问题。

内容的提问来源于stack exchange，提问作者Andy