Булево-алгебраический подход к полноте для нормальных модальных предикатных логик

Аннотация

В этой статье представлена инновационная методология для демонстрации полноты в нормальных модальных предикатных логиках. Традиционные доказательства обычно включают построение канонических моделей, в которых возможные миры определяются как максимальные непротиворечивые множества, обладающие определенными свойствами, с большой опорой на формулу Баркана для подтверждения существования этих миров. Наш подход отклоняется от классического метода, используя булевы алгебры и ультрафильтры для построения моделей. В отличие от традиционных методов, наше построение возможных миров не зависит от формулы Баркана; вместо этого данные свойства гарантируются леммой Тарского.

Кроме того, наше доказательство отличается от других булево-алгебраических доказательств полноты в двух ключевых аспектах: оно использует семантику Крипке вместо алгебраической семантики и опирается исключительно на ультрафильтры, тем самым предлагая более лаконичный подход. Эта методология способствует естественному переходу от модальной логики высказываний к модальной логике предикатов и позволяет избежать дополнительной сложности Q-фильтров. В нашей модели класс эквивалентности каждой теоремы нормальной модальной предикатной логики является членом всех миров, тогда как класс эквивалентности каждой не-теоремы является членом некоторых миров. Как следствие, структура этих миров гарантирует, что не-теоремы ложны в модели.