• English only

# Differences

This shows you the differences between two versions of the page.

 sav08:finite_models_imply_decidability [2008/04/02 17:06]vkuncak created sav08:finite_models_imply_decidability [2008/04/03 13:04] (current)vkuncak 2008/04/03 13:04 vkuncak 2008/04/02 17:06 vkuncak created 2008/04/03 13:04 vkuncak 2008/04/02 17:06 vkuncak created Line 1: Line 1: ====== Finite Models Imply Decidability ====== ====== Finite Models Imply Decidability ====== - Prover and counterexample finder running in parallel. + 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. 