With respect to a modal logic $\text{L}$, a property satisfied by $\text{L}$ when for any formula $\phi$ in the language of $\text{L}$, if there is a Kripke model with a possible world at which $\phi$ is true, then there exists a finite Kripke model (i.e., whose set of possible worlds is finite) with a world at which $\phi$ is true. When $\text{L}$ is a sound and complete modal logic that extends classical logic, this condition may be equivalently stated as the property that if ${⊭}_{\text{L}}\phi$ (i.e., $\phi$ is not an $\text{L}$-theorem), there exists a finite Kripke model with a possible world at which $\phi$ is true. That a modal logic has the finite model property is frequently an important ingredient in proving it to be decidable.