Правила вывода

Модальная система S4.

Гильбертовская формулировка HS4.

Алфавит - алфавит классического исчисления высказываний с добавлением символов □и ◊.

◊ А есть сокращение для выражения □ А.

Правильно построенные выражения – формулы.

К определению формулы классического исчисления высказываний добавляется пункт:

Если А - есть формула HS4, то выражения □(А) и ◊( А) – также являются формулами HS4.

Аксиомы.

А0. - Все тавтологии КлИВ.

Следующие две аксиомы имеются в большинстве модальных систем, которые называются нормальными модальными системами:

А1. □А А

А2. □ (А В) (□ А □ В)

Следующая специальная аксиома, по существу, и определяет HS4.

А3 (HS4). □ А □ □ А

Правила вывода.

П1. Стандартное правило (modus ponens):

П2. Правило введение необходимости:

□ A

Стандартные определения доказательства и доказуемой формулы в HS4.

Стандартные вопросы для формальных систем: разрешимость, непротиворечивость, наличие семантики, прагматика, полнота относительно семантики.

Специальный вопрос для модальных систем – структура неприводимых модальностей.

Пример. Доказать в HS4

□ (A&B) (□A & □ B)