Determine if a structure is a model of an inductively defined predicate
What do you mean by the equality in your first formula? In first-order logic (FOL) with equality, one can only apply the equality operator to a couple of terms, not to formulae. Also, your use of equality cannot be considered a case of definition (what could be better depicted by $\triangleq$) since the predicate List appears on both sides of the equality. When creating a definition, the definiendum (in the left side of $\triangleq$) should not be mentioned in the definiens (right side of the $\triangleq$).

By FOL, are you referring to the so-called "first order programming logic" (a formal system specially designed for expressing recursive functions)? Since FOL cannot express transitive closure, I cannot think of a way to properly express recursion in FOL.