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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

• ${\displaystyle {\textbf {Cl}}}$:

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

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

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

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

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

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

История

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

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

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

• ${\displaystyle {\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}}}$.

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

• ${\displaystyle {\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е годы определение «суперинтуиционистской логики» ввел А. В. Кузнецов в докладе на семинаре по математической логике в Московском университете (тогда ещё использовался термин «суперконструктивная логика»)^[3].

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

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

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

Имя	Аксиомы
${\displaystyle {\textbf {For}}}$	${\displaystyle ={\textbf {Int}}+p}$
${\displaystyle {\textbf {Cl}}}$	${\displaystyle ={\textbf {Int}}+p\lor \lnot p}$
${\displaystyle {\textbf {SmL}}}$	${\displaystyle ={\textbf {Int}}+(\lnot q\to p)\to (((p\to q)\to p)\to p)}$
${\displaystyle {\textbf {KC}}}$	${\displaystyle ={\textbf {Int}}+\lnot \lnot p\lor \lnot p}$
${\displaystyle {\textbf {LC}}}$	${\displaystyle ={\textbf {Int}}+(p\to q)\lor (q\to p)}$
${\displaystyle {\textbf {SL}}}$	${\displaystyle ={\textbf {Int}}+((\lnot \lnot p\to p)\to \lnot p\lor p)\to \lnot p\lor \lnot \lnot p}$
${\displaystyle {\textbf {KP}}}$	${\displaystyle ={\textbf {Int}}+(\lnot p\to q\lor r)\to (\lnot p\to q)\lor (\lnot p\to r)}$
${\displaystyle {\textbf {WKP}}}$	${\displaystyle ={\textbf {Int}}+(\lnot p\to \lnot q\lor \lnot r)\to (\lnot p\to \lnot q)\lor (\lnot \to \lnot r)}$
${\displaystyle {\textbf {ND}}_{k}}$	${\displaystyle {\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}}}$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

См. также

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