# Peano Arithmetic: How would this formalized statement be correct?

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.

• What are all these tildes (~)? I can't even read your attempted formulas. – BrianO Dec 14 '15 at 17:10
• 3,4 are completely different statements than 1,2 – Hagen von Eitzen Dec 14 '15 at 17:10
• Tilde (~) are negation, i.e. "it is not the case that...". @HagenvonEitzen, could you please write it in the correct form? Is 5,...,9 also wrong? – litmus Dec 14 '15 at 17:14
• @litmus I can't say much about 5,...,9 because I'm still guessing about the interpretation of $[p]q$ (is that $p\to q$?) and why the negation symbol seems to be both pre- and appended. But I'm quite confident that 5,...9 do not encode the natural language statement 1. - Is there any (online?) reference for your notation? – Hagen von Eitzen Dec 14 '15 at 17:17
• Several issues: $x$ is free in 1 (and 2), but is not free in 3 (if I interprete the "some" correctly), or it is simply a completely different property. Compare "Jack is the father of a red-head girl" with "If Jack is a red-head girl then he is the father of George" – Hagen von Eitzen Dec 14 '15 at 17:30

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

• Thank you! In this context what does the implication arrow (→) do, and how can I rewrite the statement without it? (It is not included at all in my material.) – litmus Dec 15 '15 at 9:24
• @litmus - it seems to me that Hagen has already answered to you : $p \to q$ is (in your formalization) : $[p]q$. – Mauro ALLEGRANZA Dec 15 '15 at 10:08
• My bad, sorry, I totally overlooked that. – litmus Dec 15 '15 at 10:10

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.

• Thank you for your effort @HagenvonEitzen! I understand that it is hard to help without the source, may I email you the PDF file that I am using? – litmus Dec 14 '15 at 18:13
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 1, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 1, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.8778325319290161, "perplexity": 1213.6365798797274}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2019-35/segments/1566027313617.6/warc/CC-MAIN-20190818042813-20190818064813-00030.warc.gz"}