Small formulas with large models
Take the usual language of first-order logic from introductory textbooks, without identity and function symbols. The vast majority of sentences in this language are satisfied in models with very few individuals. You even have to make an effort to come up with a sentence that requires three or four individuals. The task is harder if you want to come up with a fairly short sentence. So I wonder, for any given number n, what is the shortest sentences that requires n individuals?
The shortest sentence that requires 2 individuals is (unsurprisingly)
Fa ∧ ¬Fb
with 6 symbols. Of course there are trivial variants of that sentence that also have 6 symbols, so it's not technically the unique shortest sentence that requires 2 individuals.
The shortest sentence that requires 3 individuals has 12 symbols (not counting parentheses) and is already much harder to find. It is
∀y∃x(Ryx ∧ ¬Rxy)
Again, all other 12-symbol sentences that require 3 individuals are trivial variants of this one.
The shortest sentence that requires 4 individual, with 14 symbols, is even more ingenious:
∀z∀y∃x(Rzx ∧ ¬Rxy)
Once again, this is essentially the only 14-symbol formula that requires 4 individuals.
That's as far as I got. I don't know the shortest sentence that requires 5 individuals. I did find a nice sentence with 18 symbols though that requires 7 individuals:
∀z∀y∃x¬((Rxy → Ryx) ∨ Rzx)
I found these sentences by writing a computer program that goes through all sentences of a given length (ignoring alphabetic variants) and computes the smallest model for each. Due to the undecidability of first-order logic, there are lengths for which this program won't be able to determine an answer, but at a length of 10-20 symbols this isn't really an issue yet. I couldn't get past 15 symbols simply because of the huge number of sentences with 15+ symbols. I added some heuristics to skip over 99% of sentences, but to go beyond 15-20 symbols I think a completely new approach would be needed.
Here's a related question. Given any number n, what is the largest finite size among the smallest models for sentences with n symbols? For example, the smallest model for any 5-symbol sentence has size 1; so the largest size among all those models is 1. For 6 symbols, the answer is 2, since there is a 6-symbol sentence that requires 2 individuals. More generally, the function just defined begins as follows:
| length | largest size among smallest models |
|---|---|
| 1 | 1 |
| 2 | 1 |
| 3 | 1 |
| 4 | 1 |
| 5 | 1 |
| 6 | 2 |
| 7 | 2 |
| 8 | 2 |
| 9 | 2 |
| 10 | 2 |
| 11 | 2 |
| 12 | 3 |
| 13 | 3 |
| 14 | 4 |
| 15 | 4 |
| 16 | ? |
| 17 | ? |
| 18 | ≥7 |
As someone pointed out on stackoverflow, it follows from Trakhtenbrot's Theorem that this function is uncomputable, so it must eventually surpass every computable function, despite its dawdling beginning. It's a nice example of an uncomputable function. Maybe one should give it cute name to make it better known?