How to define multiplication in addition terms in monadic second order logic? meaning, having natural numbers variables, N sub-groups variables, successor function, negations, "for every", "there exists" and "+" operation, I need to create a formula that will describe the multiplication operation. For example, given square, "+" and "/", multiplication can be described as: a*b={(a+b)^2-a^2-b^2}/2
Thanks
A bit informally...
$x$ divides $y$ iff $y$ belongs to all sets which contain $0$ and are closed under addition-by-$x$.
$x=y^2$ iff $x+y$ is the least common multiple of $y$ and $y+1$.
$x=yz$ iff $(y+z)^2=y^2+z^2+2x$.