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.