Does anyone know an example of a mathematically interesting first order theory $T$ such that the following conditions hold?
Really, this is just a comment, but it's way too long:
First, a quick observation: assuming your language is finite, every example must be finitely axiomatizable. (Although that finite axiomatization may not be known.)
I want to give two potentially interesting classes of examples: one having a Ramsey-theoretic flavor, and the other coming from complexity theory. I'm hampered by the fact that I don't really know anything about either subject, so what follows is purely speculative.
In model theory, often we want to construct models of a given theory with nice combinatorial patterns - e.g., with indiscernible sequences of a given order-type, etc. I don't know if this is true, but I suspect that in finite model theory, finite combinatorial patterns are also important. Now, suppose I'm given a theory $T$ and a Ramsey-type theorem "Every sufficiently large structure exhibits pattern $P$." Then the 'bad' models of $\varphi$ are bounded in size - and hence the class of them is axiomatized by a single formula $\varphi$, even if $T$ is not finitely axiomatizable - but no upper bound on this size need be known. Even if an upper bound is known, there is a good chance (Ramsey theory being what it is) that it is truly terrible.
Now, I suspect that these classes of models are interesting only insofar as they make finite model theory difficult, that is, such a class might be relevant for studying the finite model theory of the corresponding theory $T$ but I doubt they are particularly interesting on their own. However, I could be wrong. (I could also be wrong that anything like this is of interest in finite model theory.) Hopefully, someone who actually knows finite model theory will set me straight on this.
Now let me give a class of potential examples coming from complexity theory.
Let $X$ be a set in some 'large' complexity class, say $NEXPTIME$. Call a Turing machine (deterministic or non) $\Phi$ an $X$-guesser if $\Phi(n)=1$ implies $n\in X$; that is, $\Phi$ may not compute $X$, but it never gives false positives.
There may be a collection $\{\Phi_i: i\in\omega\}$ of particularly nice $X$-guessers with extremely small runtime; maybe these arise in trying to 'build $X$ from below' to get a better upper bound on the complexity of $X$. If so, then if $X$ is sufficiently natural and these runtimes really are sufficiently small, we can probably prove that each $\Phi_i$ outputs 1 only finitely many times. Then, for each $i$, the set $X_i=\{n: \Phi_i(n)=1\}$ is a finite set of natural numbers; but upper bounds for these may not be known.
What does this have to do with finite models? Well, take the case where $X\in NEXPTIME$. An old result of ??? shows that the sets of the form $\{n: \exists A\models\varphi (\vert A\vert=n)\}$ (called (finite) spectra) are precisely the sets in $NEXPTIME$. So, given this sequence of sets $X_i$, starting with a formula $\varphi$ corresponding to $X$ we get formulas $\varphi_i$ corresponding to $X_i$ for each $i$. At this point, it's in principle possible that the structure of these formulas can be attacked by finite model theory more efficiently than the sets $X_i$ can be attacked from complexity theory. (Although to the best of my knowledge, this sort of idea isn't nearly as effective as one would hope.) So this would potentially give an interesting sequence of examples of your phenomenon.
I'm sticking to sequences of examples, rather than individual examples, here because I can't imagine a single $X$-guesser with such small runtime being that interesting on its own. Admittedly, I'm also very dubious that any of this is interesting, but it passes my own 'smell' test at least for now.
