Why are subclasses of first-order logic with the finite model property decidable?

Question

The title really says all: Why are subclasses of first-order logic with the finite model property decidable?

Answer 1

The finite model property says that if $\varphi$ is not provable, then there's a finite model $\mathcal{M}$ with $\mathcal{M} \models \lnot \varphi$.

So let's say we want to know if $T \vdash \varphi$ or not.

def isProvable(phi):
  n = 1
  while True:
    for p in [proofs of length n]:
      if p proves phi: return True
    for M in [models of size n]:
      if M models (not phi): return False
    n += 1

If $\varphi$ is provable, then it has a proof of finite length, so for $n$ large enough, our first case will find it and we'll return True. If $\varphi$ is not provable, then the finite model property says that for some $n$ large enough our second case will find a countermodel, and we'll return False.

Notice that, even without the finite model property, we can still try this algorithm! If $\varphi$ is provable, then we'll still find a proof eventually. But if $\varphi$ is not provable, without the finite model property our second clause is not guaranteed to find a countermodel, so our code might loop forever. This tells us that provability is always semidecidable, or if you prefer, computably enumerable (CE).

The finite model property tells us that provability is also co-CE, in the sense that non-provability is CE.

Through this lens, the above proof is a special case of a more general result that a problem is decidable exactly when it's both CE and co-CE.

---

I hope this helps ^_^