Логика предикатов
Категория реферата: Рефераты по философии
Теги реферата: bestreferat ru, роботы реферат
Добавил(а) на сайт: Пондяков.
Предыдущая страница реферата | 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 | Следующая страница реферата