Логика предикатов (стр. 6 из 7)
1 $xA(x) допущение2 A(exA(x)) $у; 1
3 $xA(x)É A(exA(x)) Éв; 1-2
4 $y($xA(x)É A(y) $в; 3
Но как хорошо известно, последняя формула не доказуема интуиционистски. Аналогично в этой системе может быть доказан принцип конструктивного подбора Маркова
Где в этих доказательствах неинтуиционистские шаги? Ответ, видимо, неоднозначен. В книге [5] я предлагал наложить ограничения на непрямые правила вывода: потребовать, чтобы e-термы не входили в устраняемые допущения и заключение. Однако это ограничение слишком стеснительно и неэлегантно. А.Г. Драгалин [1], а затем Д. Скотт ввели другое ограничение: в правилах введения квантора существования и удаления квантора общности мы должны потребовать, чтобы вводимый или исключаемый терм был не пуст. Это более изящное решение проблемы. В настоящей статье я предлагаю формулировку интуиционистского исчисления предикатов с e-символом и предикатом существования в виде субординатного вывода. Затем обсуждается проблема систематического поиска выводов в этом исчислении.
Язык интуиционистского натурального исчисления с e-символом NeI строится с помощью двух типов индивидных переменных: свободных - v,v1,v2,... и связанных - x,y,z,. . ., x1, x2, . . ., предикатных знаков, логических связок &,Ú,É,Ø, знака абсурдности ^, предиката существования E, кванторов " и $, e-символа, скобок и запятой. Одновременной индукцией определяем понятия квазитерма и квазиформулы. Термами и формулами являются квазитермы и кваиформулы, не содержащие свободных вхождений связанных переменных. Под подстановкой вместо свободной переменной v квазитерма t в квазиформулу или квазитерм имеется в виду замещение каждого вхождения свободной переменной v в квазитерм или квазиформулу квазитермом t. Подстановку будем обозначать Fv/t A и Fv/t t1. Подстановка правильна, если ни одна связанная переменная, имеющая свободные вхождения в t не находится в области действия кванторов или e-оператора по этой переменной. Ниже мы будем иметь дело только с правильными подстановками. Отметим, что каждая подстановка терма правильна. Каждую формулу, начинающуюся с квантора мы можем представить в виде "xFv/xA и $xFv/xA. Следуя Гильберту и Бернайсу, будем говорить, что терм t1 вложен в терм t2, если t2 имеет вид Fv/t1 t3, где подстановка, естественно, правильна. Например, терм exD(x) вложен в терм eyA(exD(x), y). Квазитерм exB(x,y) подчинен квазитерму eyA(y,exB(x,y)),т.е. первый квазитерм имеет свободные вхождения связанной переменной, по которой образован второй терм. В дальнейшем мы будем иметь дело с выводами, посылки и заключение которых не будут содержать e-термов. Поэтому в NeI в выводы не будут входить формулы с подчиненными друг другу квазитермами.
Вывод имеет вид субординатного вывода, при этом каждый вспомогательный вывод будет иметь не более одного допущения. Определим, что мы будем понимать под субординатной последовательностью формул (c-последовательность), вхождением в нее формулы и ее последней формулой:
1. Пустая последовательность есть с-последовательность, она не имеет последней формулы и ни одна формула не входит в нее.
2. Если A формула, то A есть последовательность формул, A есть последняя формула и формула A входит в нее.
3. Если a есть с-последовательность и A формула, то
a
A есть с-последовательность, A её последняя формула и формула B входит в нее, если она входит в a или графически равна A.
4. Если a, b и g суть с-последовательности формул и A формула, то
aa 
b и b суть с-последовательности, A их A gA
последняя формула и формула B входит в них, если она входит в a или графически равна A.
Будем говорить, что формула C непосредственно выводима из формулы A (A и B), если
есть одно из правил прямого вывода; формула C непосредственно выводима из пустого множества формул, если C есть аксиома, т.е. имеет место правило
.Теперь введем понятие натурального вывода для системы NeI.
1. A есть вывод из последовательности посылок A, A входит в A и A есть его последняя формула.
2. Если A есть аксиома, то A есть вывод из пустой последовательности посылок, A есть его последняя формула и входит в вывод.
3. Если a есть вывод из последовательности посылок G и A посылка, то
есть вывод из последовательности посылок GA, A есть его последняя формула и формула B входит в вывод, если B входит в a или графически равно формуле A.
4. Если a есть вывод из последовательности посылок G, формула C непосредственно выводима из формул, входящих в a ( или является аксиомой), то
есть вывод из последовательности посылок G, C его последняя формула и B входит в вывод, если оно входит в a или графически равно C. На применение правила введения квантора общности накладываем ограничение: если a есть вывод из последовательности посылок G, формула A(w) входит в вывод a, но в формулы из G не входит собственная переменная w, то
a
"xFw/x A(w)
есть вывод из последовательности посылок G.
5. Если a есть вывод из последовательности посылок G и b есть вывод из посылок D,A и все формулы из D входят в a, B есть последняя формула, то
есть вывод из посылок G и AÉB есть его последняя формула.
6. Если a есть вывод из посылок G, b есть вывод из посылок D1,A и g есть вывод из посылок D2,B,формулы D1 и D2 входят в a, формула C есть последняя формула b и g, то
есть вывод из посылок G и C есть его последняя формула.
7. Если a есть вывод из последовательности посылок G,A и ^ есть его последняя формула, то
есть вывод из посылок G и ØA есть его последняя формула.
Чтобы определение вывода NeC было полным необходимо сформулировать прямые правила вывода. Прежде всего есть правило тождественного перехода: из A выводима A, обозначим его буквой I. Остальные правила вывода подразделяются на правила введения и удаления логических констант. В приводимой ниже таблице правил вывода мы для полноты записываем и непрямые правила (хотя они сформулированы в определении вывода).
Кроме основных будем использовать в качестве официальных также два производных правила Éе1 и Éi2:
и 
Теперь перейдем к процедуре писка вывода. Поиск начинается с формулировки задачи: из посылок A1,...,An требуется вывести формулу В. Мы исходим из допущения, что ни посылки, ни заключение не содержат e-символов и предиката существования. Не нарушая общности можно также допустить, что они не содержат свободных переменных. Задача поиска вывода записывается в виде
Это, естественно, не вывод. Построение ( поиск ) вывода совершается с помощью двух типов шагов: синтетических и аналитических. Синтетический шаг состоит в применении некоторого прямого правила вывода. Аналитический шаг сводит задачу к подзадачам.
Сформулируем аналитические и синтетические правила поиска вывода для импликации. Задача вывода формулы AÉB из некоторой последовательности посылок сводится к подзадаче построения вывода формулы B из того же множества посылок и дополнительного допущения A. Это аналитическое правило введения импликации. Мы его запишем в виде
где n наибольший номер в первоначальной задаче. В анализе указаны официальные правила вывода (не правила поиска вывода). Аналитическое правило удаления импликации состоит в сведении задачи вывода формулы C из формулы AÉB, стоящей выше знака выводимости, к двум подзадачам: выводу формулы A из прежних посылок и выводу формулы C из прежних посылок и формулы B. Символически
Синтетическое правило удаления импликации разрешает написатьвыше знака выводимости формулу B, если формулы A и AÉB входят в фигуру заключения выше знака выводимости:
Для симметрии можно сформулировать и синтетическое правило введения импликации: если в фигуру выше знака выводимости входит формула A, то непосредственно над знаком выводимости можно написать формулу BÉA. Однако формулу B надо указать дополнительно. Символически