# The Peano Axioms in Polish Notation

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)$$
• Could you show a couple of the Peano axioms in non-Polish notation so we can be sure we understand your question?
– MJD
Commented Feb 14 at 22:32
• 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. Commented Feb 14 at 22:36
• Sorry, I will include the forms of the axioms I would like parsed Commented Feb 14 at 22:41
• 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. Commented Feb 14 at 22:53

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.
• 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. Commented Feb 14 at 23:45
• 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. Commented Feb 15 at 20:54