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.

  • $\begingroup$ What are all these tildes (~)? I can't even read your attempted formulas. $\endgroup$ – BrianO Dec 14 '15 at 17:10
  • 1
    $\begingroup$ 3,4 are completely different statements than 1,2 $\endgroup$ – Hagen von Eitzen Dec 14 '15 at 17:10
  • $\begingroup$ 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? $\endgroup$ – litmus Dec 14 '15 at 17:14
  • $\begingroup$ @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? $\endgroup$ – Hagen von Eitzen Dec 14 '15 at 17:17
  • 1
    $\begingroup$ 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" $\endgroup$ – Hagen von Eitzen Dec 14 '15 at 17:30


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

  • $\begingroup$ 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.) $\endgroup$ – litmus Dec 15 '15 at 9:24
  • $\begingroup$ @litmus - it seems to me that Hagen has already answered to you : $p \to q$ is (in your formalization) : $[p]q$. $\endgroup$ – Mauro ALLEGRANZA Dec 15 '15 at 10:08
  • $\begingroup$ My bad, sorry, I totally overlooked that. $\endgroup$ – 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.

  • $\begingroup$ 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? $\endgroup$ – litmus Dec 14 '15 at 18:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.