I'm trying to write a statement in logic symbols that says there is a unique $x$ such that $P(x)$ is true. I've heard of writing this down as $\exists !x P(x) $. But I think I'm not allowed to use the symbol $\exists !$. Now I'm trying to write an equivalent statement without using that symbol. I've come up with two statements, but I'm not sure if one of them is correct:
$\exists x ,\lnot \exists y (P(x) \land P(y) \land \lnot (x=y))$
$\exists x P(x) \land \lnot \exists y (P(y) \land \lnot (x=y))$
My doubt with the first one is that I've never seen a construction like $\exists x, \lnot \exists y (...)$.
My doubt with the second one is that I'm not sure if the variable $x$ in this part $\lnot \exists y (P(y) \land \lnot (x=y))$ is interpreted as a free variable or as the variable with the property $\exists x P(x) $.
Remember that $\lnot\exists y(\dots)$ is the same as $\forall y\lnot(\dots)$, your first one is equivalent to:
$$\exists x\forall y \left(\lnot P(x)\lor \lnot P(y)\lor(x=y)\right)$$
So, as another poster said, all you'd need is $\exists x:\lnot P(x)$ to prove this statement. So this statement is actually saying something more complicated.
The second statement is correct, although I'd mind the parentheses there:
$$\exists x \left(P(x) \land \lnot \exists y \left(P(y) \land \lnot (x=y)\right)\right)$$
and again you can replace $\lnot\exists y$ with $\forall y\lnot$, which other answers above have done.
But I prefer to think of $\exists!$ as being shorthand for "there is one, and at most one." That is, two completely separate statements joined by $\land$. So I'd write it as:
$$\left(\exists xP(x)\right)\land\forall y\forall z \left(\left(P(y)\land P(z)\right)\implies y=z\right)$$