Expansion of bounded uniqueness quantifier

I have the following rules for rewriting sentences with bounded quantifiers in arbitrary first-order languages to ordinary (unbounded) quantifiers:

\begin{align} \forall\phi(x).\psi(x)&\qquad\to\qquad\forall x.\phi(x)\implies \psi(x),\\ \exists\phi(x).\psi(x)&\qquad\to\qquad\exists x.\phi(x)\land\psi(x) \end{align}

... where $$\phi$$ and $$\psi$$ are formulae with free variable $$x$$ ($$\phi$$ is the scope of the quanitfier - e.g. $$\forall x\in\Bbb{R}.\psi(x)$$).

$$\exists!x.\phi(x)\qquad\to\qquad \exists x.\forall y.\phi(y)\iff y=x$$

I would like to expand bounded uniqueness quantifiers in arbitrary first-order languages. (i.e. $$\exists!\phi(x).\psi(x)$$) in the same way as the universal and existential quantifier.

As far as I can tell, there are two ways to do this, depending on whether I apply the rule for expanding the existential or uniqueness quantifier first (provided that these rules are appropriately modified).

Applying the rule for existential quantifiers first yields the sequence of reductions:

\begin{align} \exists!\phi(x).\psi(x)&\qquad\to\qquad\exists!x.\phi(x)\land\psi(x)\\ &\qquad\to\qquad\exists x.\forall y.(\phi(y)\land\psi(y))\iff y=x&(\textbf{fmla 1}) \end{align}

Applying the rule for uniqueness quantifiers first yields:

\begin{align} \exists!\phi(x).\psi(x)&\qquad\to\qquad\exists\phi(x).\forall\phi(y).\psi(y)\iff y=x\\ &\qquad\to\qquad\exists \phi(x).\forall y.\phi(y)\implies(\psi(y)\iff y=x)\\ &\qquad\to\qquad\exists x.\phi(x)\land\forall y.\phi(y)\implies(\psi(y)\iff y=x)&(\textbf{fmla 2}) \end{align}

Analytic tableaux shows that these are nonequivalent if $$=$$ is taken only to be an equivalence relation.

The ncatlab page on quantifiers provides the following:

$$\exists!\, x\colon T, P(x) \;\equiv\; \exists\, x\colon T, P(x) \wedge \forall\, y\colon T, P(y) \Rightarrow (x = y)$$

...which, generalizing the typing relation to arbitrary formulae, would suggest...

\begin{align} \exists!\phi(x).\psi(x)&\qquad\to\qquad\exists\phi(x).\psi(x)\land\forall\phi(y).\psi(y)\implies y=x\\ &\qquad\to\qquad\exists x.\phi(x)\land\psi(x)\land\forall\phi(y).\psi(y)\implies y=x\\ &\qquad\to\qquad\exists x. \phi(x)\land\psi(x)\land\forall y.\phi(y)\implies(\psi(y)\implies y=x) & (\textbf{fmla 3}) \end{align}

This is most similar to formula 2, but weaker due to the replacement of the bi-implication $$\psi(y)\iff y=x$$ with the implication $$\psi(y)\implies y=x$$. Analytic tableaux shows that $$\textbf{fmla 2}\implies\textbf{fmla 3}$$ if $$=$$ is taken to be an arbitrary equivalence relationship.

Countermodels

These were obtained via analytic tableaux using the program found here (github here)

Define:

$$E:=\forall x.\forall y.\forall z.R(x,x)\land(R(x,y)\implies R(y,x))\land((R(x,y)\land R(y,z))\implies R(x,z))$$

(i.e. $$R$$ is an equivalence relation)

For $$E\implies (\textbf{fmla 1}\implies\textbf{fmla 2})$$ the program timed-out

$$E\implies (\textbf{fmla 1}\implies\textbf{fmla 3})$$ is valid

For $$E\implies (\textbf{fmla 2}\implies\textbf{fmla 1})$$ we have the countermodel $$\mathcal{M}_1:=\langle D=\{0,1\}, R=D^2,\ \phi=\{0\},\ \psi=\{0,1\}\rangle$$

$$E\implies (\textbf{fmla 2}\implies \textbf{fmla 3})$$ is valid

For $$E\implies (\textbf{fmla 3}\implies \textbf{fmla 1})$$, we have the countermodel $$\mathcal{M}_2:=\langle D=\{0,1\},R=D^2,\ \phi=D,\ \psi=\{0\}\rangle$$

For $$E\implies (\textbf{fmla 3}\implies \textbf{fmla 2})$$, we have the countermodel $$\mathcal{M}_2$$

• You write "if $=$ is taken only to be an arbitrary equivalence relation". But $=$ is not an arbitrary equivalence relation, it's equality! Jul 7 '20 at 21:37
• @AlexKruckman I have this because 1) the theorem prover I am using does not have equality and 2) unique up to (equivalence relation) occurs quite frequently throughout mathematics. Jul 7 '20 at 21:51

The three formulations are all equivalent. The last one is the most intuitive variant and can be shortened in two steps to the first variant by essentially incorporating the $$\phi$$ and $$\psi$$ predications on $$x$$ into the $$\forall y$$ clause, by making the implication two-directional and saying that $$\phi$$ and $$\psi$$ must also hold if the object currently consiered is $$x$$. One may also "unsimplify" and go in the other direction from the first over the second to the third.

(1) and (2):
Transforming the biimplication into a conjunction of two implication directions:
$$A \to (B \to C)$$ is logically equivalent to $$(A \land B) \to C$$, which gives the equivalence of the $$\Longrightarrow$$ direction of the biimplication, $$𝜙(𝑦)∧𝜓(𝑦) \Longrightarrow 𝑦=𝑥$$ and $$𝜙(𝑦)⟹(𝜓(𝑦) \Rightarrow 𝑦=𝑥)$$.
The $$\Longleftarrow$$ direction can be obtained from (2) to (1) with $$\phi(x) \land \ldots$$ and $$y = x$$ by substituting $$y$$ for $$x$$ to obtain $$\phi(y) \land \ldots$$, thereby "importing" the $$\psi(x)$$ into the $$\forall y$$ clause. In the other direction from (1) to (2) one may likewise "export" and explicity specify $$\phi(x)$$, thereby resolving the dependency on $$y = x$$ and weakening the biimplication to a one-directional implication.

(2) and (3):
Analagous to above, by exporting the predication of $$\psi$$ on $$x$$ into a separate clause, the biimplication can be weakend to just the $$\Rightarrow$$ direction because now $$\psi(x)$$ is captured by an explicit predication and can do without the combination $$\psi(y)$$ and $$y = x$$.
Strenthening the implication to a biimplication with $$x = y$$ and substituting $$y$$ for $$x$$ makes it possible to go in the other direction and import the $$\psi(x)$$ into the $$\forall$$ clause.

(1) and (3) follows by transitivity.

I sketched these results with natural deduction proofs and was able to confirm the interderivability of all three; something must have gone wrong in your tableaus -- perhaps the treatment of the equality symbol?

$$M_1$$ is not a counter model of (2) $$\vDash$$ (1) because it is not a model of (2) because $$v(x) = 0$$ is the only $$x$$ such that $$\phi(x)$$, but for $$v(y) = 1$$ since $$\psi(y)$$ but not $$y = x$$ the biconditional is false and hence the formula is not true for all $$y$$.
$$M_2$$ is not a counter model of (3) $$\vDash$$ (1) because it is a model of (1) because with $$v(x) = 0$$, for $$v(y) = 0$$, both the conjunction and the equality is true and for $$v(y) = 1$$, both the conjunction and the biconditional is false, and hence for all $$y$$ the formula is true.
$$M_2$$ is not a counter model of (3) $$\vDash$$ (2) analogously.
• The tableaux was generated using a program, the same one found at (umsu.de/trees). It does not have equality, so used "$R$ is an equivalence relation" $\implies$ in the evaluation, substituting $y=x$ for $R(y,x)$. Jul 7 '20 at 21:55
• This doesn't seem to mimic rules for equivalence adequately; my first guess is that you should have used $E \land \ldots$ rather than $E \Longrightarrow \ldots$. The generated counter models are not counter models -- see the update to my post. Jul 7 '20 at 22:34