There exist sentences of first-order logic that are satisfiable and are satisfiable only by models of infinite size. However, all such sentences I can think of are satisfied by infinite models that can be generated by a non-terminating algorithm of a finite size.For a example, there exists a sentence of first-order logic that is satisfied only by a model of an infinite size:$$ \exists x \lnot \exists y S ( y, x ) \land $$$$ \forall x \exists y S ( x, y ) \land $$$$ \forall x \forall y \forall z ( ( S ( x, z ) \land S ( y, z) ) \to x = y ) $$A model for this sentence can be generated (listed, enumerated) by a finite algorithm that never terminates - just list the elements of the infinite model in a sequence one after another and make $S$ hold only for successive pairs of such elements.Does there exist a sentence of first-order logic that is satisfiable only in some infinite models for which there does not exist a finite algorithm that generates them?
Does there exist a sentence of first-order logic that is satisfiable only in infinite models that do not have a finite algorithmic representation?
lo.logic
One possible answer to your question is Tennenbaum's Theorem. It states that no non-standard model of arithmetic can have only computable operations, i.e. either addition or multiplication will be non-computable given any recursive description of the elements of the model.Now the remaining difficulty is having a single formula which has as models only non-standard models of arithmetic. Note that while arithmetic isn't finitely axiomatizable, there are conservative extensions of PA which are finite.Now it's easy to build an infinite axiomatization of (an extension of) PA which has only non-standard models: add to PA a constant $c$ and the axioms$$ c\neq 0,\ c\neq S(0),\ c\neq S(S(0)),\ldots$$There's a trick to turn this into a finite axiom. Add the binary predicate $\mathrm{NS}$ to your language, along with the axiom$$ \forall xy,\ \mathrm{NS}(x, y)\leftrightarrow x\neq y\wedge \mathrm{NS}(x, S(y))$$Then the above schema is expressed by $\mathrm{NS}(c, 0)$.Important edit: It is crucial that the induction schema (as axiomatized by your finite theory) does not apply to formulas containing $\mathrm{NC}$! Otherwise it is quite easy to show $\forall y,\ c\neq y$ and conclude $c\neq c$, a contradiction. I think that if you exclude those formulas from the induction principle, the above reasoning should go through without trouble. 