= Solution
A fragment has the <finite model property> if $\boxed{\text{every satisfiable sentence in the fragment has a finite model}}$. This does not mean that every model is finite, nor that there is one uniform bound on model size for the entire fragment.
<ALC> has the <finite model property>, including satisfiability with respect to finite <TBoxes>. A <tableau algorithm for ALC> uses finitely many possible labels and <direct blocking in description logic> to obtain a finite representation of a model. The resulting finite-model claim is a property of the logic; termination alone, for an arbitrary procedure, would not establish it.
Full <first-order logic> does not have the <finite model property>. For example, the <first-order sentence>
$$
\bigl(\forall x\,\neg R(x,x)\bigr)\land
\bigl(\forall x\forall y\forall z\,((R(x,y)\land R(y,z))\to R(x,z))\bigr)\land
\bigl(\forall x\exists y\,R(x,y)\bigr)
$$
requires an irreflexive transitive relation with a successor for every element. It is satisfied by the usual strict order on the <natural numbers>. In a nonempty finite domain, repeatedly taking successors eventually repeats an element; transitivity would then force $R(x,x)$, contradicting irreflexivity. Hence this satisfiable <first-order sentence> has no finite model.
Back to article page
