A short preface:
I'm reading the book Godel Esher Bach: Eternal Golden Braid, it describes a system which it calls Typographic Number Theory. There is a question in the book that asks to represent a statement "b is a power of two" in terms of TNT. You will probably recognize the operations of TNT at once, so I'll not spend much time describing it, only what's relevant.
Here's the formula I came up with (and the interpretation, in case I've got the formula wrong):
$$ \forall{a}\forall{b}\exists{c}\forall{d}\exists{e}:<<(b=Scc)\land\lnot(b*d=a)>\land(a=e*SS0)> $$
The $<$ and $>$ symbols are used to delimit the logic expressions. $S$ stands for successor of
, so $S0$ is 1, $SS0$ is 2 and so on. $Sx$ is a successor of $x$ whatever $x$ is.
In plain language, the formula above is meant to say: "whatever $b$ is, given it is a sum of any two $c$ and one (that is if $b$ is odd) it is not the case that it multiplied with any number $d$ can produce $a$ (does not divide $a$). Yet there have to be such number $e$ which if multiplied by two will produce $a$ ($a$ is even).
I'm not pretending to have any academic background, so please excuse me if the formulation is poor!