Peano Arithmetic: How would this formalized statement be correct? Using Peano Axioms I have formalized the following:


*

*x is the square of an odd prime number

*For some odd prime number x' , x is its square

*IF x is some odd prime number, THEN x is the square of x'

*IF x' is some odd number AND x' is some prime, THEN x is the square of x'

*[x' is some odd number AND x is some prime]x is the square of x'

*[~[x' is some odd number]~~[x' is some prime]~]x is the square of x'

*[~[~∀x'~~∀x''~~x'=(SS0*x'')]~~[x' is some prime]~]x is the square of x'

*[~[~∀x'~~∀x''~~x'=(SS0*x'')]~~[~[~∀x'~∀x''∀x'''~x'=(SSx''*SSx''')]∀x''~x'=SSx'']~]x is the square of x'

*[~[~∀x'~~∀x''~~x'=(SS0*x'')]~~[~[~∀x'~∀x''∀x'''~x'=(SSx''*SSx''')]∀x''~x'=SSx'']~]∀x'x=(x'*x')
Any input regarding my formalization process is much appreciated. Please note that I am limited to using only the symbols above.
 A: Hint
In otder to symbolize "x is the square of an odd prime number" we have to start from :

"$\text {there exists } y  \text{ such that : } (\text { prime}(y) \text{ and } \text{odd}(y) \text{ and } x=y^2)$".

Assuming that you have only the universal quantifier $\forall$, we have to use : $\sim \forall y \sim$ for the existential one.
Then, you have to proceed step-by-step.
For example :

$\text{odd}(y)$ is : $\sim \forall z \sim \ (y=z*SS0+S0)$.

And :

$\text{prime}(y)$ is : $\sim (y = S0) \land ∀z \ ∀w \ (y=z*w \to (z = S0 \lor w = S0))$.

The trick now is to remove the unwanted connective. 
We have that $p \lor q$ is $\sim p \to q$, and thus we get :

$\text{prime}(y)$ is : $\sim (y = S0) \land ∀z \ ∀w \ (y=z*w \to (\sim (z = S0) \to (w = S0)))$.

A: Too long for a comment. 
I try to determine what your formal system looks like. I guess that well-formed formulae are guided by the following grammar:
$$\begin{align}
\text{wff}&\to [\ \text{wff}\ ]\ \text{wff}\\
\text{wff}&\to {\sim}\ \text{wff}\ {\sim}\\
\text{wff}&\to \forall\ \text{var}\ \text{wff}\\
\text{wff}&\to \text{expr}\ =\ \text{expr}\\
\text{var}&\to \text{var}\ '\\
\text{var}&\to x\\
\text{expr}&\to (\ \text{expr}\ \cdot \ \text{expr}\ )\\
\text{expr}&\to (\ \text{expr}\ + \ \text{expr}\ )\\
\text{expr}&\to S\,\text{expr}\\
\text{expr}&\to \text{var}\\
\text{expr}&\to 0
\end{align}$$
and all of these have their usual interpretation, except the first two unusual notations: $[p]q$ denoted implication, i.e., $[p]q$ is true except when $p$ is true and $q$ is false (usually written as $p\to q$); and ${\sim}p{\sim}$ denotes negation, i.e., ${\sim}p{\sim}$ is true if $p$ is false and vice versa. To be more precise, one should specify the rules of inference that can be applied; also some more care would be required for the use of variables (bound, free).
Alas, if my assumptions can be confirmed as correct (which I am not sure of because the patterns I thought to have discovered do not match all examples in the OP) I could continue and elaborate how to express the desired property using this formalism.
