I wonder if descendant operation is axiomatizable (or definable) in first order logic. Descendant is:
$0, s(0), s(s(0)),...$ you know it - natural numbers and something like that ....
I was using descendant in prolog, but prolog implement recursion, which is forbidden in first order logic. Since I know (only know) that recursion is forbidden in first order logic that I expect it is not axiomatized. However, I am trying to prove it, the best by game. Can you help me ?
Edit
It did come some idea to my mind, lets look at it please:
Descendant operation is in fact some function - intuitively $\lambda n.n+1$. This function may be represented as graph:
$0->s(0)->s(s(0))->.....$ keep in mind that this graph is infinite and it is correct descendant operation.
Lets consider not correct descendant operation:
$0->s(0)->s(s(0))->...->s^{2^n+1}(0)->s^{2^{n+2}}(0)->0$
We know, that now duplicator has winning strategy on $n$ rounds, therefore this class is not definable (it means that it is no express descendant operation with only one formula FO).
However, We still don't know if this descendant operation is axiomatized (infinite set of FO formulas may be used in this case)