С.Л. Катречко
ОТ ЛОГИКИ К ТЕОРИИ ПОИСКА ВЫВОДА <**>
Теория поиска вывода (ТПВ) ‑ молодая область логики, которая, в отличие от логики, акцентирует свое внимание не на вопросе о логической корректности выводов, а на вопросе о способах построения выводов («как строить (искать) вывод?») [1].
Специфику и основные идеи ТПВ покажем на примере построения вывода формулы [р É р] исчислении P1. [P1 задается тремя аксиомами <+ 102> p É [q É p]; <+103> [s É [p É q]] É [[s É p] É [s É q]]; <+104> p É f É f É p и двумя правилами вывода: <*100> - модус поненс и <*101> - подстановка; ВЫВОД определяется как последовательность формул, каждая из которых является либо некоторой аксиомой, либо получена из предшествующих формул вывода по одному из правил вывода, последняя формула которой является искомой формулой]. В [2, стр.75] приведена следующая последовательность из 9 формул, являющаяся выводом формулы [р É р] (приведем вывод с анализом):
ВЫВОД АНАЛИЗ ВЫВОДА
1. [s É [p É q]] É [[s É p] É [s É q]] <+103>
2. [s É [r É q]] É [[s É r] É [s É q]] 1, <*101> подстановка
p/r
3. [s É [r É p]] É [[s É r] É [s É p]] 2, <*101> подстановка q/p
4. [p É [r É p]] É [[p É r] É [p É p]] 3, <*101> подстановка s/p
5. [p É [q É p]] É [[p É q] É [p É p]] 4, <*101> подстановка r/q
6. p É [q É p]
<+102>
7. [p É q] É [p É p]
5, 6 <*100>
8. p É [q É p] É [p É p] 7, <*101> подстановка q/qÉp
9. p É p 8, 6 <*100>
Давайте зададимся вопросом: «Почему на 1 (2, 3... 8) шагах были выбраны те или иные аксиомы, правила вывода и сделаны в случае выбора правила <*101> подстановки?», т.е. нас в данном случае интересует не вопрос о корректности построенного вывода, а вопрос об осмыслении процесса построения вывода. Прикладное значение этой постановки вопроса заключается в том, чтобы научить студента или ЭВМ строить подобные выводы.
Основная идея ТПВ - переход к метаисчислениям, в рамках которого появляется возможность учитывать «структурную» информацию логической формулы. Эта идея может быть реализована двумя способами:
· введением собственно допустимых, т.е. не производных, правил вывода, существенно сокращающих длину вывода;
· использованием метода временных переменных (метапеременных), которые вводятся для фиксирования (полной или неполной на данном этапе построения вывода) информации о возможной структуре выводимой формулы, а в последующем, при получении дополнительной необходимой информации, заменяются на переменные (формулы) исходного исчисления.
Остановимся более подробно на втором способе (заметим, что в [2] Черчем реализован первый путь перехода к метаисчислению путем доказательства метатеоремы дедукции, которая выступает как собственно допустимое правило вывода, позволяя вводить (а впоследствии, исключать) допущения). Для этого введем временные метапеременные, которыми при анализе структуры формулы будем заменять отдельные ее переменные (подформулы) так, что каждая эквивалентная переменная (подформула) будет заменяться на одну и ту же временную метапеременную. Отметим, что к временным метапеременным применим аналог правила подстановки (правило <*101>). При построении выводов будем использовать следующую стратегию: будем подставлять выводимую формулу в «хвост» какой-либо аксиомы или уже выведенной формулы (заметим, что на первых порах, самой полезной формулой является аксиома <+103>). За счет этого мы исходную задачу сводим к задачам получения выводов антецедентов новой формулы, которые затем можно последовательно исключить по модус поненс (правило <*100>).
Обратимся к примеру вывода формулы р É р. Применим стратегию поиска, выбрав в качестве базовой формулы аксиому <+103>. Тогда первая метаформула такова: [p É [A É p]] É [[p É A] É [p É p]], где A - временная переменная. Сформулируем задачу поиска: для получения вывода формулы р É р необходимо в выводе получить две формулы, структура первой из которых имеет вид p É [A É p], а структура второй - p É A. Заметим, что первая из указанных подзадач решается тривиально, поскольку метаформула p É [A É p] по своей структуре совпадает с вариантом аксиомы <+102>. Для решения второй подзадачи, заменим A - на метаформулу B É p, где В - новая временная переменная, тогда метаформула p É [B É p] может быть превращена в вариант аксиомы <+102>. При этом на структуру метапеременной A накладывается ограничение: A @ B É p. Метапеременную B сразу заменим на переменную q, что превратит эту метаформулу p É [B É p] в аксиому <+102>. Обе подзадачи решены, и у нас имеется необходимая информация о соответствии временных переменных и формул исходного исчисления: метапеременная A «замещает» подформулу q É p, а B - переменную q. Тем самым, ясен набор подстановок в аксиому <+103>: переменные s и q заменяем на p, а саму p - на q É p, после проведения которых мы получим формулу [p É [q É p] É p]] É [[p É [q É p] É [p É p]]; и после двух применений к ней и аксиоме <+102> (второй раз - к варианту аксиомы <+102>) правила модус поненс получим более короткий и понятный вывод формулы р É р.
================
<**> — данный текст является расширенными
онлайновой версией доклада с учетом
выступлений на международных конференциях «Развитие логики в России: итоги и
перспективы» (1997), 2-ые «Смирновские чтения» (1999).
Литература:
1. Маслов С.Ю. Теория дедуктивных систем и ее применения. - М.: Радио и связь, 1986.
2. Черч А. Введение в математическую логику. - М.: ИЛ., 1960.