# First-order logic: largest size among smallest finite models for formulas of a given length

Apologies for the somewhat cryptic title.

For any first-order formula X, let ssm(X) be the size of the smallest finite model of X. By size I mean number of individuals. So, for example, ssm('Fa & ~Fb') = 2 because the smallest models of 'Fa & ~Fb' have two individuals. If X has no model, or only infinite models, f(X) is undefined.

Now, for any number n, let lssm(n) be the maximum of ssm(X) among all formulas X with length n. That is, lssm(n) is the largest size among the smallest finite models for formulas with length n. The specifics obviously depend on details of the relevant language: whether we have function symbols, identity, redundant Boolean operators, etc. So there are in fact several different functions here.

What is known about these functions? Are they computable? Can we say approximately what value they take for, say, n=30?

• The non-computability is an asymptotic result, you can compute the values for small $n$ or for some easy languages (e.g. the empty language). Otherwise, it depends on your exact framwork, but the translation's complexity is polynomial in many cases, so there isn't much to win asymptotically. For small formulas with big smallest finite models, you can use the trick in Reinhardt, "The complexity of translating logic to finite automata" to get a family of formulas with models growing non-elementarily fast. These formulas are reasonably short, but require some work. – Graffitics Feb 6 '16 at 7:50