I am new to Polish Notation, and would like someone to translate the Peano axioms into PN for me. Either the first order or second order axioms would do, but if you can do both that would be much appreciated. I am particularly struggling to understand how to represent implication between expressions which themselves are equalities. Thanks!

Edit: Here are the first-order axioms in Infix Notation I am trying to parse:

  1. $\forall x \ (0 \neq S ( x ))$
  2. $\forall x, y \ (S( x ) = S( y ) \Rightarrow x = y)$
  3. $\forall x \ (x + 0 = x )$
  4. $\forall x, y \ (x + S( y ) = S( x + y ))$
  5. $\forall x \ (x \cdot 0 = 0)$
  6. $\forall x, y \ (x \cdot S ( y ) = x \cdot y + x )$
  7. $\forall \bar{y} \Bigg(\bigg(\varphi(0,\bar{y}) \land \forall x \Big( \varphi(x,\bar{y})\Rightarrow\varphi(S(x),\bar{y})\Big)\bigg) \Rightarrow \forall x \varphi(x,\bar{y})\Bigg)$
  • $\begingroup$ Could you show a couple of the Peano axioms in non-Polish notation so we can be sure we understand your question? $\endgroup$
    – MJD
    Commented Feb 14 at 22:32
  • 2
    $\begingroup$ That's a huge ask, supported by little evidence about what you've tried and asking us to guess what specific formalisations of PA you are interested in. As an example, here is symmetry of equality in Polish: ${\to}{=}xy{=}yx$. Or in reverse Polish $xy{=}yx{=}{\to}$. Can you take it from there? If not, then please ask a much more specific question. $\endgroup$
    – Rob Arthan
    Commented Feb 14 at 22:36
  • $\begingroup$ Sorry, I will include the forms of the axioms I would like parsed $\endgroup$ Commented Feb 14 at 22:41
  • $\begingroup$ If you see an infix move the operator to the front then use the terms as arguments. So for $x+y$ you'd write $+(x,y)$ instead. Similarly you'll use $=(x,y)$ to evaluate if $x=y$ is true. $\endgroup$ Commented Feb 14 at 22:53

1 Answer 1


The solution to the bit that you say you are struggling with is that $S(x) = S(y) \Rightarrow x = y$ is ${\Rightarrow}{=}SxSy{=}xy$ in Polish and $xSyS{=}xy{=}{\Rightarrow}$ in reverse Polish.

  • $\begingroup$ Could you also add to your answer how to parse the more complicated 7th axiom? $\endgroup$ Commented Feb 14 at 23:00
  • $\begingroup$ Why don't you try and then ask about where you went wrong? MSE is not a question-answering service. As a clue, the Polish (rather than reverse Polish) for the 7th axiom starts $\forall\overline{y}{\Rightarrow}$. If you want any more help, you could at least upvote my answer. $\endgroup$
    – Rob Arthan
    Commented Feb 14 at 23:45
  • 1
    $\begingroup$ Here's a bit more help: $ \forall x \Big( \varphi(x,\bar{y})\Rightarrow\varphi(S(x),\bar{y})$ is $\forall{\Rightarrow}\phi x \bar{y} \phi S x \bar{y}$. I think you should have enough examples now to try it yourself. $\endgroup$
    – Rob Arthan
    Commented Feb 15 at 20:54
  • $\begingroup$ Thanks, that helps. My confusion was if single valued operators with the infix between input and output worked the same way as binary operators where the infix is between two inputs, and it seems that they do. $\endgroup$ Commented Feb 15 at 22:39

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .