Showing that a certain formula of second order logic with full semantic is true in all and only non-standard model of arithmetic. Showing that a certain formula of second order logic with full semantic is true in all and only non-standard model of arithmetic.

$\exists X(\exists x Xx \wedge \forall x\forall y((Xx \wedge (x=0 \vee x=y+1)) \rightarrow (x\not=y \wedge Xy)))$

How should I approach this problem?
This should be the right answer to the question.

Suppose that the formula is true in an arbitrarily standard model $M$, then we get that there is a property $X$, such that if there is an $x$ that has that property, for every number, if $Xx$ and $x\not=0$ then also the predecessor of $x$, namely $y$ has the property $X$. Now we can iterate this reasoning, given that $Xy$ and the if $y\not=0$ then also the predecessor of $y$ has the property $X$, until we get to the case in which $x=0$. In this case the antecedent of the implication would be true, given that the left disjunct in the antecedent is true, but the consequent would be false having $0\not=0$. This is so because we know that if the successor of 0 has the property X, then also 0 must have the property X. Also we have $\forall y$ in the formula, hence we will have the case in which $y=0$. Therefore we get the implication false, and this contradicts our assumption. By the arbitrariness of the standard model $M$ we can conclude that the formula has no standard model.

Now if we assume that the formula is true in a full semantic model, then we get that it must exists a set of all the non-standard numbers, given that the interpretation of $X$ range over all the possible subsets of the power set of the domain. That is our property $X$. So it is clear that the formula must be true for all the non-standard numbers. This is so because whenever we pick a non-standard number $n^*$, it must have a predecessor, say $n_{i}^*$ (because that non-standard number cannot be 0). Now given that every successor of a standard number is standard, it follows that also $n_{i}^*$ is non-standard. By applying this reasoning over and over we get an infinite descending sequence of non-standard numbers. By a very similar reasoning this allows us to say that the formula is valid in such a model. Whenever $x$ has the property $X$ ($x$ is a non standard number), we can always find a predecessor with the property of being non-standard without ever coming to a stop. Now by arbitrariness of the model, we have that (given that no standard model satisfy the formula), the formula is true in all and only non standard models.
This should be the right answer to the question.

Suppose that the formula is true in an arbitrarily standard model $M$, then we get that there is a property $X$, such that if there is an $x$ that has that property, for every number, if $Xx$ and $x\not=0$ then also the predecessor of $x$, namely $y$ has the property $X$. Now we can iterate this reasoning, given that $Xy$ and the if $y\not=0$ then also the predecessor of $y$ has the property $X$, until we get to the case in which $x=0$. In this case the antecedent of the implication would be true, given that the left disjunct in the antecedent is true, but the consequent would be false having $0\not=0$. This is so because we know that if the successor of 0 has the property X, then also 0 must have the property X. Also we have $\forall y$ in the formula, hence we will have the case in which $y=0$. Therefore we get the implication false, and this contradicts our assumption. By the arbitrariness of the standard model $M$ we can conclude that the formula has no standard model.

Now if we assume that the formula is true in a full semantic model, then we get that it must exists a set of all the non-standard numbers, given that the interpretation of $X$ range over all the possible subsets of the power set of the domain. That is our property $X$. So it is clear that the formula must be true for all the non-standard numbers. This is so because whenever we pick a non-standard number $n^*$, it must have a predecessor, say $n_{i}^*$ (because that non-standard number cannot be 0). Now given that every successor of a standard number is standard, it follows that also $n_{i}^*$ is non-standard. By applying this reasoning over and over we get an infinite descending sequence of non-standard numbers. By a very similar reasoning this allows us to say that the formula is valid in such a model. Whenever $x$ has the property $X$ ($x$ is a non standard number), we can always find a predecessor with the property of being non-standard without ever coming to a stop. Now by arbitrariness of the model, we have that (given that no standard model satisfy the formula), the formula is true in all and only non standard models.