Q:

First order sentences and Halting problem recursively enumerable

I am just finding searching for some examples of recurisvely enumerbale models and I do not know how to prove that the following ones satisfy this property. 

Consider the set of first order sentences.  The subset of the sentences which have a finite model are recursievly enumerable
The Halting problem is recursively enumerable

Ideas: For the first one I take the universal signature $\sigma_U$ which is given by $\sigma_U^{Op}=\{f_n^k | n,k\in\mathbb N\}$, $\sigma_U^{Rel}=\{R_n^k | n,k\in\mathbb N\}$ and $ar_{\sigma_u}(f_n^k)=ar_{\sigma_u}(R_n^k)=k$ but I do not know how to go on.  
For the second one I guess this is intuitively clear because every pait from the form (Programm, Input) is recurisvely enuemrbale when the program halts with input Input.  

A:

For the first, simply enumerate all the first-order sentences and check whether they have a model of cardinality $0,1,2,\ldots$. The only slightly difficulty is that you cannot check one sentence after another because you won't reach any sentence after the first one which doesn't have a finite model.  To work around this, you have to interweave the two checks.  You can for example check all sentences of length less or equal 1 for models of cardinality 1, then all sentences of length less or equal 2 for models of cardinality 2, and so on. 
For the second problem, the same trick works.  You can enumerate all combinations of turing machines and inputs and check for each one whether it halts on $0,1,2,\ldots$ steps.  You'll again need to interweave to avoid getting stuck upon hitting the first non-halting pair machine and input.