В математической логике логика L обладает свойством конечной модели ( для краткости fmp), если любая не - теорема L фальсифицируется некоторой конечной моделью L. Другой способ выразить это — сказать, что L имеет fmp, если для каждой формулы A из L A является L - теоремой тогда и только тогда, когда A является теоремой теории конечных моделей L.
Если L конечно аксиоматизируема (и имеет рекурсивный набор правил вывода ) и имеет fmp, то она разрешима . Однако этот результат не верен, если L просто рекурсивно аксиоматизируемо. Даже если существует только конечное число конечных моделей на выбор (с точностью до изоморфизма ), все равно остается проблема проверки того, подтверждают ли базовые фреймы таких моделей логику, и это может оказаться неразрешимым, если логика не является конечно аксиоматизируемой, даже когда оно рекурсивно аксиоматизируемо. (Обратите внимание, что логика рекурсивно перечислима тогда и только тогда, когда она рекурсивно аксиоматизируема — результат, известный как теорема Крейга .)
Формула первого порядка с одним универсальным количественным определением имеет fmp. Формула первого порядка без функциональных символов , где все экзистенциальные квантификации появляются первыми в формуле, также имеет fmp. [1]