Предыдущая страница реферата | 1  2  3  4  5  6  7  8  9  10 | Следующая страница реферата

Существуют два типа систем натурального вывода: с прямым и непрямым правилом удаления квантора существования. Прямое правило удаления квантора существования по существу формулируется с использованием языка с эпсилон-символом. Классическое исчисление предикатов с прямым правилом удаления квантора существования элегантно и является хорошей основой для организации систематической процедуры поиска доказательств. Мною была предложена процедура поиска доказательств для классического исчисления предикатов с прямым правилом удаления квантора существования [7]. А.В.Смирнов и А.Е.Новодворский [3] реализовали ее на компьютере. Хотелось бы построить интуиционистское исчисление предикатов с прямым правилом удаления квантора существования и на этой основе сформулировать алгоритм поиска доказательств. Однако на этом пути мы встречаемся с определенными  трудностями. Если мы заменим классические пропозициональные правила интуиционистскими, то в результате получим логическую систему, более богатую, нежели интуиционистское исчисление предикатов. Действительно, допустим, что имеет место $xA(x). По правилу удаления квантора существования получим A(exA(x)). По правилу введения импликации будем иметь $xA(x)ÉA(exA(x)). Из последней формулы по правилу введения квантора существования получаем $y($xA(x)ÉA(y)). Запишем этот вывод формально

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 формула, то

                         a                    a

                         b         и          b  суть с-последовательности, A их

                         A                    g       

                                                 A

последняя формула и формула B входит в них, если она входит в a или графически равна A.

Будем говорить, что формула C непосредственно выводима из формулы A (A и B), если

есть одно из правил прямого вывода; формула C  непосредственно выводима из пустого множества формул, если C есть аксиома, т.е. имеет место правило   .

Теперь введем понятие натурального вывода  для системы  NeI.

1. A есть вывод из последовательности посылок  A, A входит в A и A есть его последняя формула.

Рекомендуем скачать другие рефераты по теме: сочинение изложение, курсовые работы бесплатно.





Предыдущая страница реферата | 1  2  3  4  5  6  7  8  9  10 | Следующая страница реферата