правила для модальности

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

Генценовский вариант GS4.

Алфавит: такой же как и КлИВ с добавлением символа секвенции и символов модальностей □ и ◊.

Правильные выражения: секвенции- выражения вида , где - списки формул S4 (возможно пустые).

Аксиомы: все секвенции вида

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

Правила введения и удаления логических связок.

Все правила введения и удаления указанные при формулировке СКИП, в сукцеденте которых может использоваться список формул . Например,

а) Введение &:

б) Удаление &:

и т. д.

правила для модальности.

удаление □: введение □:

Г, А → ∆ □ Г→ А

Г, □ А→∆ □ Г→ □А, где □ Г – список формул, каждая из

которых в качестве главной связки

имеет модальность □.

3) все структурные правила СКлИВ без изменений(сокращения в антецеденте и сукцеденте, утончения в антецеденте и сукцеденте, перестановки в антецеденте и сукцеденте, сечения).

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

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

Специальные вопросы: связь с HS4, устранение сечения.