The paper discusses the notion of finite model truth
definitions (or FM-truth definitions), introduced by
M. Mostowski as a finite model analogue of Tarski’s classical
notion of truth definition.
¶
We compare FM-truth definitions with Vardi’s concept of the
combined complexity of logics, noting an important difference:
the difficulty of defining FM-truth for a logic ℒ does not
depend on the syntax of ℒ, as long as it is decidable. It
follows that for a natural ℒ there exist FM-truth
definitions whose evaluation is much easier than the combined
complexiy of ℒ would suggest.
¶
We apply the general theory to give a complexity-theoretical
characterization of the logics for which the Σdm classes
(prenex classes of higher order logics) define FM-truth. For any
d≥ 2, m≥ 1 we construct a family {[Σdm]≤
k}k∈ω of syntactically defined fragments of Σdm
which satisfy this characterization. We also use the
[Σdm]≤ k classes to give a refinement of known results
on the complexity classes captured by Σdm.
¶
We close with a few simple corollaries, one of which gives a
sufficient condition for the existence, given a vocabulary σ,
of a fixed number k such that model checking for all first order
sentences over σ can be done in deterministic time nk.