Свойство конечной модели - Finite model property

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

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

Пример

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

Смотрите также

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

Рекомендации

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

1. Леонид Либкин, Элементы теории конечных моделей, глава 14