I need some help on where to begin with the following question:
We say that a list (term) represents the natural number $k$ in binary if it consists of constants 0 and 1 and the digits of the binary expansion of $k$ are listed in reverse order. For example both the lists $[1,0,1,1]$ and $[1,0,1,1,0,0]$ represent the number $13$ (written backwards in binary), as $13=1+4+8$; the lists $[\ ]$, $[0]$, and $[0,0,0]$ represent $0$, etc.
Write a set of first-order clauses $\Sigma$ that define a predicate $INC(x,y)$ in such a way that $INC(t,s)$ is entailed by $\Sigma$ whenever $t$ and $s$ are list representations of natural numbers in binary and the value represented by $s$ is one bigger than the value represented by $t$.
Would I begin defining some way to write (in first order logic) that $s$ is a larger number than $t$, and that $s,t \in \mathbb{N}$?