1

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.

litmus
  • 671
  • What are all these tildes (~)? I can't even read your attempted formulas. – BrianO Dec 14 '15 at 17:10
  • 1
    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
  • I might end with something like $\exists p\langle x=(p\cdot p)\land \langle\forall k \neg p=k+k\land \forall a\forall b\neg p=(SSa\cdot SSb)\rangle\rangle \rangle $ – Hagen von Eitzen Dec 14 '15 at 17:23
  • @HagenvonEitzen, thanks. the [p]q menas IF p THEN q. I cannot find the pdf publicly online, what is wrong when going from 2 to 3? – litmus Dec 14 '15 at 17:26
  • Ok, wow, that includes a lot of symbols we have not touched upon. – litmus Dec 14 '15 at 17:29
  • 1
    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
  • Hmm, ok, I think I understand, thank you @HagenvonEitzen! Would you mind terribly if I asked you to try formalizing the statement using only the symbols I have used (these are the only ones we have been taught). – litmus Dec 14 '15 at 17:35

2 Answers2

2

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

Mauro ALLEGRANZA
  • 94,169
1

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.

Hagen von Eitzen
  • 374,180
  • 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