Finite Models Imply Decidability

Now for some positive results.

Theorem: Suppose that $S$ is a subset of all first-order logic sentences such that for all $F \in S$ ,

$\lnot F \in S$ , and
if $F$ has a model, then $F$ has a finite model

Then there exists an algorithm that, given a formula from $F \in S$ , determinies whether $F$ is valid.

Note: such algorithm is called a decision procedure for the class of formulas $S$ .

Note: we have just shown that such algorithm does not exists for the set of all sentences in first-order logic. There is only an algorithm (e.g. resolution) that will terminate when formula is valid, but need not terminate on invalid formulas.

Proof:

Prover and counterexample finder running in parallel.