Свойство конечной модели

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

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

Формула первого порядка с одной универсальной квантификацией имеет fmp. Формула первого порядка без функциональных символов , где все экзистенциальные квантификации появляются первыми в формуле, также имеет fmp. ^[1]

• Семантика Крипке

• Патрик Блэкберн, Мартен де Рийке , Иде Венема Модальная логика . Издательство Кембриджского университета, 2001.
• Аласдер Уркухарт . Разрешимость и свойство конечной модели. Журнал философской логики , 10 (1981), 367-370.