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:
- $\forall x \ (0 \neq S ( x ))$
- $\forall x, y \ (S( x ) = S( y ) \Rightarrow x = y)$
- $\forall x \ (x + 0 = x )$
- $\forall x, y \ (x + S( y ) = S( x + y ))$
- $\forall x \ (x \cdot 0 = 0)$
- $\forall x, y \ (x \cdot S ( y ) = x \cdot y + x )$
- $\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)$
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.