Проблема построения семантики для модального исчисления B

Специфика модальных исчислений

Одним из направлений развития современной логики стала разработка модальных логик.

Первые идеи в сфере модальной логики принадлежат Аристотелю. Философ предложил наряду с ассерторическими силлогизмами использовать модальные силлогизмы – силлогизмы, в которых хотя бы одна посылка представляет собой высказывание типа:

• «А возможно принадлежит В»,
• «А необходимо принадлежит В».

Аристотель не рассматривал необходимое как возможное. Ученик Аристотеля, Теофраст, развил эти идеи, начав относить модальность не к отдельным понятиям, а к высказываниям в целом. Он принял тезис, что все необходимое возможно. Это позволило определить возможность через необходимость: «возможно А» стало трактоваться как «не необходимо не-А».

Средневековая логика разделила модальности на две категории:

• de dicto (о речи) – модальности, которые относятся к высказыванию в целом;
• de re (о вещи) – модальности, которые относятся к свойствам.

Основу современных исследований модальной логики заложил К. Льюис, который построил исчисления S1-S6. В качестве характерного примера можно указать исчисления S4 и S5 (трактовка К. Геделя). Построение этих исчислений производится путем расширения классических логик высказываний и предикатов. В язык логики были введены:

• модальный оператор □ (необходимость), который действует на предложения языка;
• модальный оператор ◊ (возможность), который является сокращением ¬□ ¬.

Определение формулы было дополнено пунктом, что если А является формулой, то □А также является формулой.

Для получения аксиоматики пропозиционального модального исчисления аксиомные схемы и правила вывода, сформулированные в классической логике высказываний, дополняются:

• модальной схемой аксиом □(А⊃В) ⊃ (□A⊃□B);
• правилом вывода «если доказуемо A⊃В, то доказуемо □A⊃□B», получившим название «правило С».

Такое пропозициональное модальное исчисление называется С2.

Если заменить правило С на более сильное правило вывода (правило Геделя) «доказуемо А→ доказуемо □А» и добавить одну из аксиомных схем:

• □A⊃A,
• □A⊃□□A,
• ¬□А⊃□¬□A,

будет получено пропозициональное модальное исчисление Т, S4 и S5 соответственно.

Добавление модальных приставок к классической логике предикатов порождает ряд проблем, поскольку при этом в предикатных модальных контекстах может быть нарушен закон подстановочности тождественных ∀х∀у(х = у ⊃ (F(x) ⊃ F(y)).

Подходы к построению семантики для модального исчисления В

Одной из проблем при построении семантики для модального исчисления B является неоднозначность интерпретации модальных операторов. Например, в одной интерпретации «необходимо» может означать, что утверждение верно во всех возможных мирах, в то время как в другой интерпретации это может означать, что утверждение верно только в одном определенном мире. Также возможны различные интерпретации оператора «возможно», которые могут привести к разным выводам о возможных состояниях системы.

Другой проблемой является построение семантики для модального исчисления B в контексте динамических систем, где состояния системы могут изменяться со временем. В этом случае необходимо учитывать не только текущее состояние системы, но и ее возможные будущие состояния.

Для решения этих проблем были предложены различные подходы к построению семантики для модального исчисления B, такие как:

• семантика Крипке,
• семантика Гарднера.

Первый значимый шаг в построении семантики для модального исчисления был сделан Р. Карнапом. На основе идей Лейбница он построил семантику для множества описаний состояний (положений дел, который характеризуются языковыми средствами, или «возможных миров»). Семантически высказывание «возможно А» характеризуется им как «А является истинным по крайней мере в одном возможном мире», а высказывание «необходимо А» - как «А истинно во всех возможных мирах».

С. Крипке отказался от того, чтобы обязательно представлять возможные миры как описания состояний, зависящие от структуры логического языка. Такое представление он сохранил только для канонических моделей (максимально непротиворечивых множеств), в то время как общем случае рассматривал возможный мир как элемент произвольного непустого множества. При этом допускается, что у такого множества есть изолированные элементы (элементы, не связанные ни с какими другими элементами рассматриваемого множества).

Чтобы выразить эту идею формально, С. Крипке ввел отношение достижимости – бинарное отношение, определимое для множества возможных миров. Обозначив отношение достижимости R, можно записать следующее: если для миров a и b имеет место aRb, то из мира а можно достичь мир b; эти миры связаны. В противном случае из мира a невозможно достичь мир b. При описанном подходе формальные семантики для разных модальных исчислений отличаются тем, какие свойства имеет отношение R. Так, чтобы получить адекватную семантику для S4, достаточно предположить, что отношение R рефлексивно и транзитивно. Если дополнительно предположить симметричность этого отношения, то получим адекватную семантику для S5. В этом последнем случае каждый возможный мир достижим из каждого, и надобность в специальном отношении достижимости отпадает. Предложенная Карнапом формальная модальная семантика соответствует этому частному случаю и годится, следовательно, только для S5.

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