Интуиционистское исчисление высказываний

В этой главе мы рассмотрим формальные системы, которые внешне похожи на формализации исчисления высказываний (системы ИВ и КИВ), но тем не менее значительно от них отличаются. Эти системы являются формальными аналогами интуиционистской логики высказываний.

Интуиционизм — это такое направление в основаниях математики, которое запрещает использование некоторых способов рассуждения, применяемых в классической математике. Наиболее ярким примером является запрет на использование принципа исключённого третьего. Основанные на этом принципе доказательства неконструктивны. Приведём один из самых известных примеров такого рода.

Задача 2.1. Докажите, что существуют два таких иррациональных числа а, 6, что а^ь рационально.

Решение. Рассмотрим число а = (у/2)^. Если оно рационально, то утверждение доказано. В противном случае «V² = (л/2)² = 2 рационально.

Хотя мы доказали утверждение, мы не указали никакой пары искомых чисел. Рассуждения такого типа интуиционисты отвергают. В частности, они считают дизъюнкцию двух утверждений доказанной лишь в том случае, когда предъявлено доказательство одного из них.

Другой яркий пример ограничений в рассуждениях интуиционистов — запрет на использование закона двойного отрицания. Предположим, что доказано утверждение «неверно, что не существует алгоритма для решения задачи Л». Классическая логика позволяет сделать вывод, что такой алгоритм существует. Интуиционисты отказываются признавать этот вывод.

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

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