序列演算规则正确性验证及推理逻辑合理性咨询

参考说明：我正在学习Ebbinghaus所著的《Mathematical Logic》，采用以下正确性定义：
一个矢列 $\Gamma\vdash\phi$（原文写为$\Gamma\phi$，应为标准矢列记法的笔误）被称为正确的，当且仅当 $\Gamma\models\phi$（注：原文表述“$\Gamma$ is some other sequent”有误，实际$\Gamma$是一组公式的集合）

核心问题 #

判断以下推导规则是否正确：
$$\frac{\phi \quad \psi}{\exists x\phi \quad \exists x\psi}$$

我已经得出该规则正确的结论，推理逻辑如下。请帮我判断这个逻辑是否有误，以及是否过度复杂化了问题。

我将问题拆解为四种情况，基于自由变元$x$在$\phi$和$\psi$中的存在性：

• (i) $x \in \text{free}(\phi)$ 且 $x \in \text{free}(\psi)$
• (ii) $x \notin \text{free}(\phi)$ 且 $x \notin \text{free}(\psi)$
• (iii) $x \notin \text{free}(\phi)$ 且 $x \in \text{free}(\psi)$
• (iv) $x \in \text{free}(\phi)$ 且 $x \notin \text{free}(\psi)$

各情况的推理分析：

1. 情况(i)：显然成立。推导结论中的两个存在量化式，可以直接使用前提中满足$\phi$和$\psi$的同一个见证（witness）来验证。
2. 情况(ii)：显然成立。当$x$不在公式的自由变元中时，$\exists x\alpha$和$\alpha$是逻辑等价的，因此前提和结论中的对应公式完全等价，规则自然成立。
3. 情况(iii)：结论中的$\exists x\phi$可以取任意元素作为见证——因为任何满足$\phi$的模型都满足$\psi$，而$\phi$不含自由的$x$，意味着$x$的赋值可以任意变化，所以无论$x$取何值，$\phi$的真值都不受影响，$\exists x\phi$必然为真；同时$\exists x\psi$可由前提$\psi$直接推出。
4. 情况(iv)：这是我最不确定的部分：$\psi$不依赖于$x$的赋值，只要前提中的$\psi$为真，$\exists x\psi$就等价于$\psi$（因为$x$不是$\psi$的自由变元），所以必然为真；而$\exists x\phi$则可由前提中的$\phi$直接推出——只要$\phi$在某个赋值下为真，就存在对应的$x$见证使得$\exists x\phi$成立。

我认为四种情况都成立，因此该推导规则是正确的。主要对情况(iv)的解释存疑，希望能得到相关帮助。

备注：内容来源于stack exchange，提问作者martinkleins