The problem is this:
By defintion $ \neg(\exists ! y F(x,y))\quad \leftrightarrow \quad \forall y\neg((F(x,y) \wedge \forall z (F(x,z) \rightarrow y=z))) $
I don't see how $\neg F(x,y)\quad \leftrightarrow \quad \exists z (F(x,z)\wedge \neg z = y)$?
Some background for the problem:
This question is from Boolos' The Logic of Provability p.27 where he is going through Peano Arithmetics.
In the question $F(x,y)$ is $\Sigma_{0}$ formula and pseudoterm (i.e. it captures some functions not found in the language of PA).
Obviously $\vdash_{PA}\exists ! y F(x,y)$ (this is the definition of pseudoterm).
Then $ \neg F(x,y)$ should be equivalent to the $\Sigma$ formula $\exists z (F(x,z)\wedge \neg z = y)$.
On a intuitive level I feel it's correct but I can't give deduction for it nor can I give waterproof explanation for it.
We have: $∃!yF(x,y)$ that is: $∃y[F(x,y) ∧ ∀z(F(x,z) → y=z))]$.
Thus, assume $∃z(F(x,z) ∧ ¬z=y)$ and assume: $F(x,y)$.
From the first one we get: $F(x,z)$ and $¬z=y$. From $F(x,z)$ and $F(x,y)$, knowing that $∃!yF(x,y),$ we have: $z=y$.
Contradiction; thus, we conclude with: $\lnot F(x,y)$.
For the other direction: Assume $\lnot F(x,y)$.
From $∃!yF(x,y),$ we get $F(x,z)$. Now assume $F(x,z) \to z=y$; by modus ponens and equality we have: $F(x,y)$.
Contradiction; thus, we conclude with $\lnot (F(x,z) \to z=y)$, equivalent to: $(F(x,z) \land \lnot z=y)$.
By $\exists$-intro we get: $∃z(F(x,z) ∧ ¬z=y)$ and we can close the initial $\exists$-elim.