Суперинтуиционистские логики

Суперинтуиционистская логика — это пропозициональная логика, содержащая аксиомы интуиционистской логики ${\textbf {Int}}$ и являющаяся её расширением. Исследование суперинтуиционистских логик началось после результата К. Гёделя, согласно которому для ${\textbf {Int}}$ не существует линейной алгебраической семантики с конечным набором значений. Построенные К. Гёделем независимые формулы побудили интерес исследовать целые классы логик, которые сперва называли «промежуточными», поскольку с точки зрения теории множеств эти логики располагаются по включению между ${\textbf {Int}}$ и классической пропозициональной логикой ${\textbf {Cl}}$. Термин «суперинтуиционистская логика» ввел А. В. Кузнецов.

Основные понятия

Язык пропозиционального исчисления ${\mathcal {L}}$ содержит следующие примитивные символы:

• множество пропозициональных переменных $\{p_{0},p_{1},\dots \}$ и константу ложь $\bot$
• пропозициональные связки: $\{\land ,\lor ,\to \}$
• две скобки: ( и ).

Вместо переменных с индексами порой используются буквы латинского алфавита: $p,q,r,s...$, а правильно построенные формулы определяются индуктивно:

• все переменные и константа ложь $\bot$ являются атомарными формулами;
• если $\varphi$ и $\psi$ являются формулами, тогда $(\varphi \land \psi ),(\varphi \lor \psi ),(\varphi \to \psi )$ также формулы.

Отрицание вводиться как импликация ко лжи $\lnot \varphi =\varphi \to \bot$.

Множество переменных обозначается ${\textbf {Var}}$, а множество правильно построенных формул ${\textbf {For}}$.

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

• modus ponens: ${\tfrac {\varphi ,\;\varphi \to \psi }{\psi }}$, или проще: имея формулы $\varphi$ и $(\varphi \to \psi )$, мы получаем $\psi$;
• правило подстановки (substitution rule): по данной формуле $\varphi$, мы получаем результат ${\textbf {s}}$$(\varphi )$,

где ${\textbf {s}}$ это отображение ${\textbf {s}}\colon {\textbf {Var}}\longrightarrow {\textbf {For}}$, которое определяется индукцией по построению формулы $\varphi$: ${\textbf {s}}p={\textbf {s}}(p)$ для любой переменной $p\in {\textbf {Var}}$, ${\textbf {s}}\bot =\bot$, ${\textbf {s}}(\chi \odot \psi )=({\textbf {s}}\chi \odot {\textbf {s}}\psi )$, где $\odot \in \{\land ,\lor ,\to \}$. Смысл правила подстановки в том, что вместо переменных некоторой формулы мы можем подставлять любые другие формулы ${\textbf {For}}$. Подстановка ${\textbf {s}}(p)=\psi$ в формуле $\varphi$ может быть записана $\varphi \{\psi /p\}$.

Определение логики

Логика $L$ — это множество формул, содержащее некоторый список аксиом и замкнутое относительно modus ponenens и правила подстановки ${\textbf {s}}$.

Определение суперинтуиционистской логики

Как исчисление

Суперинтуиционистская логика в языке ${\mathcal {L}}$ это множество формул $L$, удовлетворяющее следующим условиям:

• ${\textbf {Int}}\subseteq L$;
• $L$ замкнута относительно правила modus ponens: из $\varphi \in L$ и $(\varphi \to \psi )\in L$ следует $\psi \in L$;
• $L$ замкнута относительно правила подстановки: $\varphi \in L$ влечет ${\textbf {s}}\varphi \in L$, для каждой $\varphi \in {\textbf {For}}$ и каждой подстановки ${\textbf {s}}$.

Имеет место следующая

Теорема. ${\textbf {Int}}$ $\subseteq L\subseteq {\textbf {Cl}}$ для каждой непротиворечивой суперинтуиционистской логики $L$.

С точки зрения данного определения ${\textbf {Cl}}$ также является суперинтуиционистской. Её можно получить различными способами.

• ${\textbf {Cl}}$:

= ${\textbf {Int}}+\neg \neg p\to p$ (снятие двойного отрицания)

= ${\textbf {Int}}+(\neg p\to p)\to p$ (Consequentia mirabilis)

= ${\textbf {Int}}+p\lor \lnot p$ (закон исключенного третьего, tertium non datur)

где символ $+$ означает добавление новой аксиомы или списка аксиом с замыканием по modus ponens и правилу подстановки.

Семантически

С другой стороны, большой класс суперинтуиционистских логик может быть задан семантическим путем. Например, Г.Ф. Росс получил следующее вложение множеств логик ${\textbf {Int}}\subseteq R\subseteq M\subseteq {\textbf {Cl}}$, где $R$ рекурсивно реализуемые формулы, а $M$ множество пропозициональных формул, полученных с помощью логических матриц. Простейшей семантикой для суперинтуиционистских логик являются шкалы Крипке. Существуют топологические семантики, окрестностные, алгебраические.

История

Исследования суперинтуиционистских логик начались с теоремы К. Гёделя о нетабличности ${\textbf {Int}}$. Этот результат показал, что не существует конечного набора значений, относительно которого полна ${\textbf {Int}}$. Для доказательства данного факта Гёдель использовал занумерованный список формул, где $n>2$, и доказал их независимость друг от друга:

${\textbf {g}}{\ddot {\textbf {o}}}_{n}=\bigvee \limits _{1\leq i<j\leq n}(p_{j}\leftrightarrow p_{i})$

Исследуя этот метод, Т. Умезава начал рассматривать целый класс суперинтуиционистских логик, который он назвал «промежуточные логики». В самом деле, если использовать формулы ${\textbf {g}}{\ddot {\textbf {o}}}_{n}$ в качестве новых аксиом, то мы получим цепь логик ${\textbf {G}}{\ddot {\textbf {o}}}_{n}$, иногда называемых «гёделевыми», которые располагаются в промежутке по включению между ${\textbf {Int}}$ и ${\textbf {Cl}}$:

• ${\textbf {Int}}\subseteq \dots \subseteq {\textbf {G}}{\ddot {\textbf {o}}}_{n}\subseteq \dots \subseteq {\textbf {G}}{\ddot {\textbf {o}}}_{4}\subseteq {\textbf {G}}{\ddot {\textbf {o}}}_{3}\subseteq {\textbf {Cl}}$.

Майкл Даммит построил логику ${\textbf {LC}}={\textbf {Int}}+(p\to q)\lor (q\to p)$ и установил, что ${\textbf {LC}}$ содержится во всех гёделевых логиках:

• ${\textbf {Int}}\subseteq {\textbf {LC}}\subseteq \dots \subseteq {\textbf {G}}{\ddot {\textbf {o}}}_{n}\subseteq \dots {\textbf {G}}{\ddot {\textbf {o}}}_{4}\subseteq {\textbf {G}}{\ddot {\textbf {o}}}_{3}\subseteq {\textbf {Cl}}$.

В 60е годы определение «суперинтуиционистской логики» ввел А. В. Кузнецов в докладе на семинаре по математической логике в Московском университете (тогда ещё использовался термин «суперконструктивная логика»).

Предпринимались различные попытки описать множество суперинтуиционистских логик, пока В. А. Янков не доказал, что имеет место следующая

Теорема. Существует континуум различных суперинтуиционистских логик.

Список стандартных суперинтуиционистских логик

Имя	Аксиомы
${\textbf {For}}$	$={\textbf {Int}}+p$
${\textbf {Cl}}$	$={\textbf {Int}}+p\lor \lnot p$
${\textbf {SmL}}$	$={\textbf {Int}}+(\lnot q\to p)\to (((p\to q)\to p)\to p)$
${\textbf {KC}}$	$={\textbf {Int}}+\lnot \lnot p\lor \lnot p$
${\textbf {LC}}$	$={\textbf {Int}}+(p\to q)\lor (q\to p)$
${\textbf {SL}}$	$={\textbf {Int}}+((\lnot \lnot p\to p)\to \lnot p\lor p)\to \lnot p\lor \lnot \lnot p$
${\textbf {KP}}$	$={\textbf {Int}}+(\lnot p\to q\lor r)\to (\lnot p\to q)\lor (\lnot p\to r)$
${\textbf {WKP}}$	$={\textbf {Int}}+(\lnot p\to \lnot q\lor \lnot r)\to (\lnot p\to \lnot q)\lor (\lnot \to \lnot r)$
${\textbf {ND}}_{k}$	${\begin{aligned}={\textbf {Int}}+(\lnot p&\to \lnot q_{1}\lor ...\lor \lnot q_{k})\to \\&\to (\lnot p\to \lnot q_{1})\lor ...\lor (\lnot p\to \lnot q_{k}),k\geq 2\end{aligned}}$

Основные свойства

Решетка суперинтуиционистских логик

Совокупность всех суперинтуиционистских логик между ${\textbf {Int}}$ и классической логикой ${\textbf {Cl}}$ образуют дистрибутивную решетку относительно включения $\subseteq$.

Дизъюнктивное свойство

Логика $L$ обладает дизъюнктивным свойством, если

$(\varphi \lor \psi )\in L\Rightarrow \varphi \in L~{\text{ или }}~\psi \in L$

Дизъюнктивным свойством обладает интуиционистская логика ${\textbf {Int}}$, но не обладает классическая ${\textbf {Cl}}$. Существует бесконечное множество суперинтуиционистских логик, обладающих дизъюнктивным свойством.

Разрешимость

Логика $L$ разрешима, если для каждой пропозициональной формулы $\varphi$ существует алгоритм, который распознает $\varphi \in L$ или $\varphi \not \in L$. Интуиционистская логика ${\textbf {Int}}$ и классическая ${\textbf {Cl}}$ разрешимы. Р. Харроп доказал, что если логика конечно аксиоматизируема и финитно аппроксимируема (finite model property), тогда она разрешима. Одновременно Р. Харроп построил логику с конечным набором аксиом, которая не обладает свойством финитной аппроксимируемости. Из чего следует, что, используя метод конечных моделей, нельзя показать разрешимость произвольной формулы для логики Р. Харропа. Существуют другие примеры конечно аксиоматизируемых, но неразрешимых логик.

Интерполяционное свойство

Логика $L$ обладает интерполяционным свойством, если $(\varphi \to \psi )\in L$, то существует формула $\chi$, содержащая только переменные общие для формул $\varphi$ и $\psi$, что

$(\varphi \to \chi )\in L~{\text{ и }}~(\psi \to \chi )\in L$.

А если формулы $\varphi$ и $\psi$ не содержат общих переменных, тогда

$\lnot \varphi \in L~{\text{ или }}~\psi \in L$.

Л. Л. Максимова установила, что существует ровно 7 суперинтуиционистских логик, обладающих интерполяционным свойством Крейга:

${\textbf {Cl}}$
${\textbf {LC}}$	$={\textbf {Int}}+(p\to q)\lor (q\to p)$
${\textbf {KC}}$	$={\textbf {Int}}+\lnot \lnot p\lor \lnot p$
$L_{1}$	$={\textbf {Int}}+p\lor (p\to (q\lor \lnot q))$
$L_{2}$	$=L_{1}+(p\to q)\lor (q\to p)\lor (p\leftrightarrow \lnot q)$
$L_{3}$	$=L_{1}+\lnot \lnot p\lor \lnot p$
${\textbf {Int}}$

Функциональная полнота

Формула $\varphi$ называется выразимой через список формул $\Gamma =\{\varphi _{1},\dots ,\varphi _{n}\}$ в суперинтуиционистской логике $L$, если $\varphi$ можно получить из $\varphi _{1},\dots ,\varphi _{n}$ посредством конечного числа замен на эквивалентные в $L$ и конечного числа подстановок в ранее полученные формулы вместо переменных. Более точно, для $\varphi _{i}$ выполняется одно из четырех условий:

• $\varphi _{i}$ переменная;
• $\varphi _{i}\in \Gamma$;
• существуют такие $j,k<i$ и переменная $p$, что $\varphi _{i}=\varphi _{k}\{\varphi _{j}/p\}$;
• существует такая $l$, что $(\varphi _{i}\leftrightarrow \varphi _{l})\in L$.

Список формул $\Gamma$ является функционально полным, если всякая формула в логике $L$ выразима через $\Gamma$.

Алгоритмическая проблема функциональной полноты разрешима для ${\textbf {Int}}$ и некоторых других суперинтуиционистских логик.

См. также

• Интуиционизм
• Теорема Гливенко

Литература

• Логический вывод / В.А. Смирнов (отв. ред.) и др. — М.: Наука, 1979. — 311 с.
• Chagrov A., Zakharyaschev M. Modal logic. — Oxford: Clarendon press, 1997. — Т. 35. — ISBN ISBN 978-0-19-853779-3.