Главная страница
qrcode

поиск доказательств в натуральном интуиционистском исчислении предикатов с е символом и предикатом существования. В. А. Смирнов Поиск доказательств в натуральном интуиционистском исчислении предикатов с - символом и предикатом существования1


Скачать 222.5 Kb.
НазваниеВ. А. Смирнов Поиск доказательств в натуральном интуиционистском исчислении предикатов с - символом и предикатом существования1
Анкорпоиск доказательств в натуральном интуиционистском исчислении предикатов с е символом и предикатом существования
Дата16.12.2017
Размер222.5 Kb.
Формат файлаdoc
Имя файлаsmirnov_epsilon.doc
ТипДокументы
#12
Каталогlibrary/logic

С этим файлом связано 1 файл(ов). Среди них: smirnov_epsilon.doc, kanger.zip.
Показать все связанные файлы

В.А. Смирнов

Поиск доказательств
в натуральном интуиционистском исчислении предикатов с
- символом и предикатом существования1


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

1 xA(x) допущение

2 A(xA(x)) у; 1

3 xA(x) A(xA(x)) в; 1-2

4 y(xA(x) A(y) в; 3

Но как хорошо известно, последняя формула не доказуема интуиционистски. Аналогично в этой системе может быть доказан принцип конструктивного подбора Маркова

1 x(A(x)  A(x)) посылка

2 xA(x) посылка

3 A(xA(x)) допущение

4 xA(x) допущение

5 A(xA(x)) у; 4

6  в; 3,5

7 xA(x) в; 4-6

8  в ;2,7

9 A(xA(x)) в; 3-8

10 A(xA(x))  A(xA(x)) у; 1

11 A(xA(x)) допущение . 12 xA(x) в; 11

13 A(xA(x)) допущение

14  в; 9,13

15 xA(x) у; 14

16 xA(x) у;11-12, 13-15

Где в этих доказательствах неинтуиционистские шаги? Ответ, видимо, неоднозначен. В книге [5] я предлагал наложить ограничения на непрямые правила вывода: потребовать, чтобы -термы не входили в устраняемые допущения и заключение. Однако это ограничение слишком стеснительно и неэлегантно. А.Г. Драгалин [1], а затем Д. Скотт ввели другое ограничение: в правилах введения квантора существования и удаления квантора общности мы должны потребовать, чтобы вводимый или исключаемый терм был не пуст. Это более изящное решение проблемы. В настоящей статье я предлагаю формулировку интуиционистского исчисления предикатов с -символом и предикатом существования в виде субординатного вывода. Затем обсуждается проблема систематического поиска выводов в этом исчислении.

Язык интуиционистского натурального исчисления с -символом NI строится с помощью двух типов индивидных переменных: свободных - v,v1,v2,... и связанных - x,y,z,. . ., x1, x2, . . ., предикатных знаков, логических связок &,,,, знака абсурдности , предиката существования , кванторов  и , -символа, скобок и запятой. Одновременной индукцией определяем понятия квазитерма и квазиформулы. Термами и формулами являются квазитермы и кваиформулы, не содержащие свободных вхождений связанных переменных. Под подстановкой вместо свободной переменной v квазитерма t в квазиформулу или квазитерм имеется в виду замещение каждого вхождения свободной переменной v в квазитерм или квазиформулу квазитермом t. Подстановку будем обозначать Fv/t A и Fv/t t1. Подстановка правильна, если ни одна связанная переменная, имеющая свободные вхождения в t не находится в области действия кванторов или -оператора по этой переменной. Ниже мы будем иметь дело только с правильными подстановками. Отметим, что каждая подстановка терма правильна. Каждую формулу, начинающуюся с квантора мы можем представить в виде xFv/xA и xFv/xA. Следуя Гильберту и Бернайсу, будем говорить, что терм t1 вложен в терм t2, если t2 имеет вид Fv/t1 t3, где подстановка, естественно, правильна. Например, терм xD(x) вложен в терм yA(xD(x), y). Квазитерм xB(x,y) подчинен квазитерму yA(y,xB(x,y)),т.е. первый квазитерм имеет свободные вхождения связанной переменной, по которой образован второй терм. В дальнейшем мы будем иметь дело с выводами, посылки и заключение которых не будут содержать -термов. Поэтому в NI в выводы не будут входить формулы с подчиненными друг другу квазитермами.

Вывод имеет вид субординатного вывода, при этом каждый вспомогательный вывод будет иметь не более одного допущения. Определим, что мы будем понимать под субординатной последовательностью формул (c-последовательность), вхождением в нее формулы и ее последней формулой:

1. Пустая последовательность есть с-последовательность, она не имеет последней формулы и ни одна формула не входит в нее.

2. Если A формула, то A есть последовательность формул, A есть последняя формула и формула A входит в нее.

3. Если  есть с-последовательность и A формула, то



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

4. Если ,  и  суть с-последовательности формул и A формула, то

 

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

A 

A

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

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



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

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

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

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

3. Если  есть вывод из последовательности посылок  и A посылка, то



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

4. Если  есть вывод из последовательности посылок , формула C непосредственно выводима из формул, входящих в  ( или является аксиомой), то



есть вывод из последовательности посылок , C его последняя формула и B входит в вывод, если оно входит в  или графически равно C. На применение правила введения квантора общности накладываем ограничение: если  есть вывод из последовательности посылок , формула A(w) входит в вывод , но в формулы из  не входит собственная переменная w, то



xFw/x A(w)

есть вывод из последовательности посылок .

5. Если  есть вывод из последовательности посылок  и  есть вывод из посылок ,A и все формулы из  входят в , B есть последняя формула, то



есть вывод из посылок  и AB есть его последняя формула.

5. Если  есть вывод из посылок ,  есть вывод из посылок 1,A и  есть вывод из посылок 2,B,формулы 1 и 2 входят в , формула C есть последняя формула  и , то



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

6. Если  есть вывод из последовательности посылок ,A и  есть его последняя формула, то



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

Чтобы определение вывода NC было полным необходимо сформулировать прямые правила вывода. Прежде всего есть правило тождественного перехода: из A выводима A, обозначим его буквой I. Остальные правила вывода подразделяются на правила введения и удаления логических констант. В приводимой ниже таблице правил вывода мы для полноты записываем и непрямые правила (хотя они сформулированы в определении вывода).

Правила введения и удаления логических знаков для NI





































Кроме основных будем использовать в качестве официальных также два производных правила е1 и i2:

и
Теперь перейдем к процедуре писка вывода. Поиск начинается с формулировки задачи: из посылок A1,...,An требуется вывести формулу В. Мы исходим из допущения, что ни посылки, ни заключение не содержат -символов и предиката существования. Не нарушая общности можно также допустить, что они не содержат свободных переменных. Задача поиска вывода записывается в виде



Это, естественно, не вывод. Построение ( поиск ) вывода совершается с помощью двух типов шагов: синтетических и аналитических. Синтетический шаг состоит в применении некоторого прямого правила вывода. Аналитический шаг сводит задачу к подзадачам.

Сформулируем аналитические и синтетические правила поиска вывода для импликации. Задача вывода формулы AB из некоторой последовательности посылок сводится к подзадаче построения вывода формулы B из того же множества посылок и дополнительного допущения A. Это аналитическое правило введения импликации. Мы его запишем в виде

где n наибольший номер в первоначальной задаче. В анализе указаны официальные правила вывода (не правила поиска вывода). Аналитическое правило удаления импликации состоит в сведении задачи вывода формулы C из формулы AB, стоящей выше знака выводимости, к двум подзадачам: выводу формулы A из прежних посылок и выводу формулы C из прежних посылок и формулы B. Символически

Синтетическое правило удаления импликации разрешает написатьвыше знака выводимости формулу B, если формулы A и AB входят в фигуру заключения выше знака выводимости:



Для симметрии можно сформулировать и синтетическое правило введения импликации: если в фигуру выше знака выводимости входит формула A, то непосредственно над знаком выводимости можно написать формулу BA. Однако формулу B надо указать дополнительно. Символически

Если в фигуру поиска вывода выше знака выводимости входит формула A и A стоит ниже знака выводимости, то знак выводимости выбрасывается - это правило исключения знака выводимости

Если A стоит непосредственно над |-, то нижнее вхождение A и знак выводимости опускаются.

Если в фигуре поиска вывода нет вхождений знака |-, то фигура поиска будетвыводом. При этом анализ дан в терминах официальных правил вывода. Ниже в таблице формулируются правила поиска вывода для связок, кванторов и предиката существования.


Syntetic

Analitic







Introduction

Elimination

Introduction

Elimination


















































w не входит в допущ.

































Специфически интуиционистскими являются аналитические правила удаления импликации, введение дизъюнкции, правило добавления заключения (вместо классического аналитического правила удаления отрицания), а также правила для кванторов и, естественно, правило для предиката существования. При формулировке кванторных правил используются временные переменные,  -термы и свободные переменные. К сожалению, мы не можем обойтись без свободных переменных и сформулировать правило введения квантора общности в виде

если A(xA(x)), то xA(x).

Помимо перечисленных в таблице правил поиска вывода, имеются также два правила удаления знака :

,

правило введения произвольной формулы



и, наконец, правило глбальной подстановки вместо временных переменных термов: во всем дереве поиска вывода разрешается заменить все вхождения временной переменной на терм.

В отличие от классической логики интуиционистские правила не обратимы. Поэтому не безразличен порядок применения правил поиска вывода. Например, пусть требуется из AB вывести BA. Если мы начнем решать задачу, применив сначала аналитическое правило введения дизъюнкции, то мы придем в тупик и не решим решаемую задачу.Однако задача последовательности применения правил поиска вывода решаема. По существу система аналитических правил есть иная формулировка логистического секвенциального исчисления. С.К. Клини [2] исследовал проблему перестановочности применений логических правил для интуиционистской логики. Опираясь на его результаты мы можем разбить правила на следующие группы :

1. правила удаления |- ;

2.Синтетические правила и аналитические правила введения конъюнкции, импликации, отрицания, квантора общности, аналитическое правило удаления дизъюнкции;

3.Аналитическое правило введения квантора существования;

4. Аналитические правила удаления импликации и отрицания;

5.Аналитическое правило введения дизъюнкции;

6.Правило введения произвольной формулы.

В каждом вспомогательном выводе отдается предпочтение правилам группы с меньшим номером. Если порядок применения правил нарушается, то поиск вывода может не дать искомого результата.

В отличие от классической логики, для поиска выводов в которой имеется одна фигура, в предложенной системе поиска для интуиционистской логики имеется правила “или”-ветвления. Это требует разработки новых програмных средств по сравнению с классической логикой

Литература

1. А.Г. Драгалин. Интуиционистская логика и - символ Гильберта.// История и методология естественных наук. М.,МГУ,1979.

2.С.К. Клини. Перестановочность применений правил в генценовских исчислениях LK и LI.// Математическая теория логического вывода. М., Наука, 1967.

3.А.В. Смирнов, А.Е. Новодворский. Язык описания логических систем.// Логические исследования, вып.3, М.1995.

4.А.В. Смирнов. Система интерактивного доказательства теорем.// Логические исследования, вып.2, М.,Наука, 1993.

5.В.А. Смирнов. Формальный вывод и логические исчисления.М., Наука, 1972.

6.V.A. Smirnov. Theory of Quantification and -calculi.// Essays on mathematical and philosophical logic. Synthese Library, vol.122, D. Reidel P.C.1979.

7.В.А. Смирнов. Поиск доказательств.// Логика и компьютер.М., Наука, 1990.

1Работа выполнена при поддержке Российского Фонда фундаментальных исследований, грант 93-06-10708.




перейти в каталог файлов


связь с админом