Here's the image:
I know its interpretation is "Some x is not P", but to me, it seems that the enclosure reads:
There is no x that is P, $\neg \exists x Px$
And then you add an extra line of identity that is defined as being the same as the one inside the enclosure:
There is a y so that there is no x so that x is y and y is P, $ \exists y \neg \exists x(=xy \space \text {&} \space Py)$
I know this reading is either wrong, or at least logically equivalent to $ \exists x \neg P x$, but I can't solve it either way.
Can you give me an explanation of the correct interpretation?
The interpretation of lines of identity going inside cuts is indeed not completely straightforward, but here is the correct way to think about this:
Whenever you have such a line, trace it to its most 'outside' context. This can be seen as the 'introduction' of that object: it is when the object's existence is being asserted. When the line goes inside some cut, then that is used to make reference to that object.
In this case, the most outside context is the very outside canvas; the Sheet of Assertion. So, the fact that there is a line a this level means that we immediately assert the existence of this object. However, the line then goes inside a cut amd is attached to a $P$. As such, we are denying that the object, whose existence was being asserted earlier, has property $P$.
In sum, there is an object, but that object does not have property $P$. In classicL notation: $\exists x \ \neg P(x)$
Another way of looking at this is as follows.... and I think this will be a little closer to what you were trying to do. OK, so we have a cut with a line inside, and so we could read this as the negation of the existence of some object, i.e. as $\neg \exists y$
But wait! There is more going on inside the cut: the line is attached to a $P$, and so what we have inside the cut is not just the existence of some object, but the existence of some object with property $P$, and it is all that that the cut is negating, i.e. we have $\neg \exists y \ P(y)$
This is an important point: a cut is the negation of whatever is represented inside the cut. So, a cut is not negating each of the invidual pieces that are inside the cut, but rather it is negating the whole of what os inside the cut.
Thus, for example, a cut with both a $P$ and a $Q$ inside is the negation of the juxtaposition, and thus conjunction, of $P$ and $Q$. That is, we have $\neg (P \land Q)$, rather than $\neg P \land \neg Q$
Likewise, the fact that we had more going on than just an object inside the cut (i.e. that we are negating something 'more' than just the existence of some object) does not mean that we are negating something in addition to the negation of some object, but rather that what is being negated is a claim that says something more than just the existence of some object.
As such, we thus have $\neg \exists y \ P(y)$, rather than something like $\neg \exists y \land \neg \exists z \ P(z)$
But wait! It's not $\neg \exists y \ P(y)$ either, because there is still more going on: The inside line is attached to an outside line. Thus, we also have an identity statement as part of what is inside the cut: the $y$ is equal to some $x$ ... whose existence is asserted outside ... and this 'earlier' (or, if you want: the 'inside' object $y$ occurs within the 'scope' of the 'outside' object $x$. Thus, we have: $\exists x (\neg \exists y (P(y) \land y=x))$
And this is exactly what you got as well! Good job!
But this last statement, you'll find, is equivalent to just $\exists x \ \neg P(x)$
Why is it equivalent? Well, unfortunately the standard equivalence principles for first-order logic are not strong enough to show this equivalence. However, using some standard inference rules, it's not hard to show this equivalence with a formal derivation.