Są.
Aby pokazać równoważność, pokażmy implikacje w obie strony.
\forall x (\psi \Rightarrow \phi) \Rightarrow (\exists x \psi) \Rightarrow \phi
Do założeń wkładamy \forall x (\psi \Rightarrow \phi) i \exists x \psi, chcemy pokazać, że \phi.
Ponieważ w \phi nie ma wolnych wystąpień x, jeśli uda nam się udowodnić, że jest spełniona dla pewnego x, będziemy mogli twierdzić, że jest spełniona dla dowolnego x, czyli niezależnie od niego - „odczepiamy” ją od x.
Weźmy więc taki x, że \psi (jego istnienie mamy zapewnione w jednym z założeń).
Dla każdego x mamy \psi \Rightarrow \phi, więc w szczególności jest tak dla naszego x.
Ponieważ \psi, mamy \phi, co należało wykazać.
[(\exists x \psi) \Rightarrow \phi] \Rightarrow \forall x (\psi \Rightarrow \phi)
Tu podobnie, mamy założone, że \exists x \psi
Możemy też założyć, że dla dowolnego x jest \psi (bo wpp. \psi \Rightarrow \phi jest prawdą). Chcemy pokazać, że \phi.
Skoro wybraliśmy jakieś x takie, że \psi, to znaczy, że istnieje takie x, że \psi.
Z (\exists x \psi) \Rightarrow \phi mamy, że \phi. QED
A podobno to można też nie wprost robić. Ale dowody nie wprost są dla słabych :>