Ограниченное исчисление ИИВ

Рассмотрим вначале ограниченное интуиционистское исчисление высказываний ИИВ_>. Эта формальная система является аналогом формальной системы ИВ. Её определение даётся по описанному во введении шаблону.

Алфавит ИИВ_>. состоит из.

• • счётного множества L пропозициональных букв;
• • пропозициональной связки —> (импликация);
• • символа лжи JL;
• • скобок — открывающей (и закрывающей).

Формулы ИИВ_). определяются аналогично формулам ИВ: формула является либо переменной, либо _1_, либо имеет вид (А—>В). Более подробное определение формулы ИИВ_> выглядит так.

Слово А в алфавите ИИВ_> является формулой тогда и только тогда, когда выполняется одно их трёх условий.

• 1: А является переменной;
• 2: А является символом лжи;
• 3: А является импликацией, т. е. имеет вид (В—>С).

Замечание 2.1. Наличие символа _1_ позволяет обойтись без отрицания. В дальнейшем мы используем ~А как сокращение для А—"±. Аналогично можно было бы поступить и в случае классического исчисления высказываний.

Аксиом в формальной системе ИИВ_> бесконечно много. Они задаются, как в случае ИВ, тремя схемами.

Формула является аксиомой ИИВ_>, если её можно представить одним из следующих способов (используем сокращённую запись формул):

где А, В, С — некоторые формулы.

Первые две схемы аксиом совпадают с аксиомами ИВ, поэтому мы их обозначили так же, как и раньше.

Правило вывода в ИИВ_> остаётся тем же самым — modus ponens.

Если рассмотреть стандартную интерпретацию формул как булевых функций, полагая, что JL соответствует тождественному 0, то легко видеть, что схема аксиом (I) является тавтологией. Таким образом, в ИИВ_". выводимы только тавтологии. Из-за отсутствия в аксиоматике схемы аксиом (АЗ) не все тавтологии выводимы в ИИВ_>. Примером такой тавтологии может служить сама аксиома (АЗ). Для доказательства невыводимости (АЗ) в ИИВ_". нам потребуется семантика моделей Кринке.

Замечание 2.2. В аксиоматике И11В_> неявно присутствует ослабленный вариант аксиомы (АЗ), который в КИВ был обозначен как (Р10) (см. с. 54):

Действительно, после раскрытия сокращения 1 эта формула запишется как.

что является частным случаем аксиомы (А2).