Peano Arithmetic: How would this formalized statement be correct?

Question

Using Peano Axioms I have formalized the following:

1. x is the square of an odd prime number

2. For some odd prime number x' , x is its square

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

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

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

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

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

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

9. [~[~∀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.

Answer 1

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)))$.

Answer 2

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.