# 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?

## 1 Answer

In general, because of Trakhtenbrot's theorem , these functions are not computable. Since with one binary relation symbol you can encode Turing machines with a logical sentence, your problem reduces to the busy beaver functions . It is known that these functions grow ridiculously fast, and that they are not computable.

 https://en.wikipedia.org/wiki/Trakhtenbrot's_theorem

• Thanks! I hadn't heard of Trakhtenbrot's theorem. I'm still curious just how fast these functions grow: it's true that the Busy Beaver function grows extremely fast, but encoding any Turing machine in first-order logic requires a lot of symbols. I certainly can't think of a reasonably short ("one line") first-order formula whose smallest finite model has size >1000, say. – Wolfgang Schwarz Feb 5 '16 at 5:50
• If you are asking "are there short sentences with finite models but only very large finite models", I think you could usefully ask that as a separate question. – Rob Arthan Feb 5 '16 at 23:50
• 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