Конечное свойство модели
В математической логике логика L обладает свойством конечной модели (для краткости fmp), если любая теорема L L. фальсифицируется конечной моделью некоторой - не Другой способ выразить это — сказать, что имеет fmp, если для каждой A языка L A формулы является L - теоремой тогда и только тогда, когда A является теоремой теории конечных моделей L. L
Если L конечно аксиоматизируема (и имеет рекурсивный набор правил вывода ) и имеет fmp, то она разрешима . Однако этот результат неверен, если L просто рекурсивно аксиоматизируемо. Даже если существует только конечное число конечных моделей на выбор (с точностью до изоморфизма ), все равно остается проблема проверки того, подтверждают ли базовые фреймы таких моделей логику, и это может оказаться неразрешимым, если логика не является конечно аксиоматизируемой, даже когда оно рекурсивно аксиоматизируемо. (Обратите внимание, что логика рекурсивно перечислима тогда и только тогда, когда она рекурсивно аксиоматизируема — результат, известный как теорема Крейга .)
Пример
[ редактировать ]Формула первого порядка с одним универсальным количественным определением имеет fmp. Формула первого порядка без функциональных символов , где все экзистенциальные квантификации появляются первыми в формуле, также имеет fmp. [1]
См. также
[ редактировать ]Ссылки
[ редактировать ]- Патрик Блэкберн, Мартен де Рийке , Иде Венема Модальная логика . Издательство Кембриджского университета, 2001.
- Аласдер Уркхарт . Разрешимость и свойство конечной модели. Журнал философской логики , 10 (1981), 367–370.
- ^ Леонид Либкин , Элементы теории конечных моделей , глава 14