Катречко С.Л.
1. Об одной модификации аксиоматического исчисления P1
2. ПОИСК ВЫВоДА в исчислении P1: стратегии, тактики, примеры
Теория поиска вывода (ТПВ) — достаточно молодая область логики (более точно: на стыке логики и эвристики), которая, в отличие от логики, не ставит своей задачей (на основе выявления логической формы) правильных способов рассуждений, а акцентирует свое внимание на прагматической стороне отношения выводимости — вопросе «как строить (искать) вывод?» — с целью повышения эффективности поисковых процедур [о теории поиска вывода см. работу: Маслов С.Ю. Теория дедуктивных систем и ее применения, М.: Радио и связь, 1986]. Одной из базовых идей в этом направлении является переход от исчислений к метаисчислениям, за счет чего удается явным образом представить необходимую для убыстрения поиска вывода информацию о структуре формуле. Как правило при этом переходе формулируются новые понятия и (на их основе) допустимые правила.
Приведем один небольшой, но очень наглядный пример, взятый из работы американского логика Р. Вейхрауха [Weyhrauch R.W. Prolegomena to a theory of mechanized formal reasoning //Artificial Intelligence, 1980, Vol.13. — p. 133—170]. Пусть нам дано аксиоматическое исчисление:
аксиома 1: A º A A [B], B º С
аксиома 2: (A º B) º (B º A) правило вывода: --------------------,
аксиома 3: (A º (B º C) º ((A º B) º C) А [С],
в котором необходимо построить вывод формулы W: (P º Q) º ((Q º R) º (R º P))
Как пишет Вейхраух, вывод формулы W в данном исчислении занимает около двух страниц. Однако задача поиска (построения) вывода значительно упрощается, если ввести новое — метауровневое — понятие «четность» (невыразимое в языке исходного исчисления) и сформулировать следующее эффективное метаправило:
Каждое высказывание W, построенное только из пропозициональных переменных с помощью связки эквивалентности " º " таким образом, что любая пропозициональная переменная p входит в W четное число раз (выделено курсивом мной — К.С.), является теоремой.
Теперь вместо (нормального) вывода формул задачу поиска можно свести к элементарному подсчету "четности" разных переменных проверяемой формулы W, что существенно сокращает ее "вывод" (поиск вывода), или вернее, заменяет «вывод» на другую, более эффективную, и допустимую в исходном исчислении процедуру.
Изложения нашей модификации известного пропозиционального исчисления А. Черча P1 [Черч А. Введение в математическую логику. М.: ИЛ., 1960] начнем с воспроизводства черчевского примера построения вывода р É р (закона рефлексивности) в P1.
Исходное исчисление P1 содержит три аксиомы:
<+102> p É [q É p]
<+103> [ s É [p É q]] É [[s É p] É [s É q]]
<+104> p É f É f É p
и два правила вывода:
<*100> Из [A É В] и А следует В (правило модус поненс)
<*101> Если b — переменная, то из А следует S b/B A | (правило подстановки)
Выводом называется последовательность формул, каждая из которых является либо некоторой аксиомой, либо получена из предшествующих формул вывода по одному из правил вывода, последняя формула которой является искомой формулой.
Приведем вывод формулы +120 [ р É р ] с анализом:
[см. А. Черч, стр. 75, а также фрагмент книги, где приводится вывод и даются комментарии самого А. Черча в приложении ]
Вывод: Анализ вывода:
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. (А. Черч Введение в математическую логику. Т. 1. М.: ИЛ, 1960. — стр.75 — 76):
Доказательством теоремы +120 является следующая последовательность девяти формул:
s É [p É q] É < s É p É < s É q
s É [r É q] É < s É r É < s É q
s É [r É p] É < s É r É < s É p
p É [r É p] É < p É r É < p É p
p É [q É p] É < p É q É < p É p
p É < q É p
p É q É < p É p
p É [q É p] É < p É p
p É p
Здесь ппф подвергнуты сокращению в соответствии с соглашениями, принятыми в предыдущем параграфе, и при проверке доказательства читатель должен представлять их себе переписанными в несокращенной форме (или, если необходимо, должен переписать их так).
Так как имеются эффективные методы проверки, то теоретически достаточно просто выписать само доказательство без дополнительных пояснений, как это и сделано выше. Однако в помощь читателю мы дадим ниже подробное разъяснение. Первая из этих девяти ппф есть +103. Следующую ппф мы получаем из первой посредством *101, подставляя r вместо р. Далее, третья ппф получена из второй подстановкой р вместо q. Четвертая получена из третьей подстановкой р вместо s. Пятая получена из четвертой подстановкой q вместо r. Шестая ппф есть +102. Седьмая получается по модус поненс из пятой как большой посылки и из шестой как малой посылки. Затем восьмая ппф получается из седьмой опять посредством применения *101, причем q É p подставляется вместо q. Наконец, p É p получается по модус поненс из восьмой и шестой ппф как большой и малой посылок соответственно.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Однако зададимся вопросом: «Почему на 1 (2, 3,..., 8) шагах были выбраны те или иные аксиомы, правила вывода и сделанные в случае выбора правила <*101> подстановки?», т.е. нас в данном случае интересует вопрос не о правильности вывода (что составляет предмет логики), а вопрос об осмыслении процесса построения вывода (прикладное значение такой постановки вопроса заключается в том, как нам научиться (или научить студента, ЭВМ) строить подобные выводы?).
Отвечая на этот вопрос, можно сформулировать следующий тезис: для этого, в общем случае, необходим переход к метаисчислению, в рамках которого появляется возможность работать с металогической формой, учитывающей «структурную» информацию логической формулы. Именно это позволяет решить вопрос о путях осмысления построения вывода.
Можно выделить и еще один путь осмысленного построения выводов — формулировку собственно допустимых правил вывода, хотя и в этом случае неявным образом предполагается использование метаязыка. Именно этот путь реализовал сам А. Черч, доказав метатеорему дедукции о допустимости ее как «поискового» правила вывода в исходном исчислении (при наложении некоторых ограничений на использовании правила подстановки), хотя и отказался от формулировки собственно метаисчисления, ограничившись показом на нескольких примерах более осмысленного, чем ранее, подхода к построению выводов [cм. А. Черч, стр. 84—85; заметим, что формулировка этого метаисчисления представляет не только технический интерес, т.к. здесь появляется возможность применения не только метатеоремы дедукции, но «надстройки» исчисления над левой, от знака выводимости, частью (т.е. над вводимыми по правилу дедукции допущениями)].
<Заметим, что правила подстановки и теорема дедукции образуют своеобразный «конфликт»: «расширяя» исходного исчисление за счет теоремы дедукции, мы «сужаем» сферу действия правила подстановки, а вводя в метаисчислении аналог правила подстановки непонятно как применить теорему дедукции.>
Введение временных метапеременных. В рамках подхода, связанного с построением метаисчислений и учетом «структурной» информации формулы, появляется еще одна интересная возможность — использование так называемых временных (или метауровеневых) переменных [первоначально эта идея была реализована С. Кангером при формулировке минус-кванторных правил в секвенциальных исчислениях], функция которых заключается в фиксировании неизвестной на данном этапе построения (поиска) вывода информации о конкретной структуре формулы; и в последующей их замене на обычные подформулы при получении такой информации.
Поясним это на примере работы в указанном исчислении А. Черча Р1. Для этого введем метапеременные, которыми при анализе структуры формулы будем заменять отдельные переменные (подформулы) так, что каждая эквивалентная переменная (подформула) будет заменяться на одну и ту же свою метапеременную (далее метапеременные обозначены заглавными латинскими буквами A, B, C >. Причем, к временным метапеременным также применим аналог <*101>: правило как бы «обратной» подстановки — подстановки вместо подформул (возможно переменных) метапеременных. Для построения вывода будем использовать следующий метод поиска (эвристику): для получения вывода формулы необходимо подставить эту формулу в «хвост» варианта какой-либо аксиомы (уже выведенной формулы) исчисления (прежде всего, <+103>) с целью получения в ходе поиска вывода предшествующих антецедентов этой аксиомы (формулы), которые затем можно последовательно исключить по правилу <*100>.
<Заметим, что в дальнейшем «сфера действия» это эвристики может быть расширена за счет использования не только <+103>, но при этом неопределенность нашего выбора существенно увеличивается, на этом же этапе применение эвристики однозначно.>
Обратимся к приведенному выше примеру вывода формулы [ р É р ]. Выберем в качестве базовой аксиому <+103>. Применим введенный метод поиска. Тогда первая метаформула будет такова: [p É [ A É p]] É [[p É A ] É [p É p]], где A — временная метапеременная (в каком-то смысле, эта метаформула соответствует формуле п.5 вывода). Сформулируем задачу поиска: для получения вывода формулы [ р É р ] необходимо в выводе получить две формулы, структура первой из которых имеет вид p É [ A É p], а структура второй — p É A. Заметим, что первая из указанных задач решается тривиально, поскольку метаформула p É [ A É p] по своей структуре совпадает с вариантом аксиомы <+102>, причем на метапеременную A не накладывается никаких ограничений и она может быть заменена на любую формулу исходного исчисления. Чуть сложнее обстоит дело со второй задачей, поскольку метаформула p É A «впрямую» не соответствует никакой аксиоме, однако можно заметить, что она «похожа» на аксиому <+102>, если в этой метаформуле метапеременную A заменить на метаформулу B É p. Тогда и в этом случае метаформула p É[ B Ép] может быть превращена в вариант аксиомы <+102>. При этом на структуру временной метапеременной A (с учетом решения второй подзадачи) уже накладывается следующее ограничение: A @ B Ép, что необходимо учесть при решении первой (уже в принципе решенной) подзадачи; а на временную метапеременную B никаких ограничений не накладывается, хотя целесообразно ее сразу заменить на переменную q, что превратит эту метаформулу в аксиому <+102>. Обе подзадачи решены, и у нас имеется достаточно информации о том, какие подформулы соответствуют двум введенным временным метапеременным: A «замещает» подформулу q É p, а B — переменную q. Тем самым, ясен набор подстановок в аксиому <+103> переменные s и q заменяем на p, а саму p — на q É p. В результате таких подстановок мы получим формулу [p É [q É p]É p]] É [[p É[q É p] É [p É p]], которая после двух применений правила модус поненс (т.е. отделения двух антецедентов по варианту и самой аксиоме +102)) даст вывод искомой формулы р É р. Несложно написать соответствующий проведенному «поисковому» анализу вывод (с анализом) в исчислении Р1:
1. [s É [p É q]] É [[s É p] É [s É q]] <+103>
2. [p É [[q É p] É p]] É [[p É [q É p]] É [p É p]] 1, одновр. <*101> p/q É p, s/p, q/p,
3. p É [q É p] <+102>
4. p É [[q É p] É p]] 3, <*101> q/q É p,
5. [p É [q É p]] É [p É p] 2, 4 <*100> (modus ponens)
6. p É p 5, 3 <*100> (modus ponens)
=== теорема доказана ===
ПОИСК ВЫВоДА в P 1: стратегии и тактики поиска; примеры выводов
Продолжим обсуждение (анализ) приведенного выше доказательства +120 (|— pÉp) так как здесь, помимо введения временных (мета)переменных для выявления структур подстановок, мы неявным образом использовали и способ решения Черча в приводимом им выводе < 120>. Назовем его общей эвристикой и сформулируем ее так:
Для доказательства некоторой ппф, необходимо данную ппф подставить в «хвост» самой «богатой» аксиомы +103, и тогда решение исходной задачи можно свести к решению двух подзадач, а именно: решению подзадачи (j1) по выводу первого антецедента полученной после подстановки в +103 варианта этой аксиомы; и решению подзадачи (j2) по выводу второго антецедента варианта +103 (понятно, что при решении подзадач применением правила модус поненс искомый вывод формулы находящейся в «хвосте» варианта аксиомы +103 будет получен).
Покажем, как используется эта эвристика при поиске вывода уже доказанной +120.
Искомая задача выглядит так: p É p. При подстановке ппф p É p в хвост аксиомы +103 (при этом мы «выписываем» вариант этой аксиомы как бы наоборот — т.е. «справа налево» — попутно подставляя временные метапеременные вместо неизвестных еще формул) получаем следующий ее вариант [p É [A É p]] É [[p É A] É [p É p]], а исходная задача редуцируется к решению подзадач:
j1: |— [p É [A É p]]
j2: |— [p É A]
При этом задача j1 решается тривиально, т.к. структура формулы соответствует структуре аксиомы +102, т.е. j1 решается как вариант +102, а задача j2 может быть решена при «замене» временной метапеременной A на формулу В É p, содержащую другую метапеременную В (см. оформление этой «схемы» решения выше).
В свою очередь, из этой эвристики «извлечем» общую стратегию решения задач в исчислении Р1 (и в любом подобном исчислении, где существенным образом используется знак импликации) <запишем стратегию в метаязыке>:
Для решения задачи |— A É С ее можно редуцировать к решению двух подзадач: j1: |— A É В и j2: |— В É С, т.е. необходимо найти такую «вставку» — формулу В — между формулами А и С, при которой обе указанные подзадачи решаются.
«Вставка» В называется формулой сечения, т.к. эта стратегия соответствует применению правила сечения (или правила транзитивности импликации), при котором для решения задачи вводится новая (заранее неизвестная!) формула — «вставка».
<Как будет показано ниже, эта стратегия может быть названа стратегией сечения 1, т.к. «вставка» формулы сечения осуществляется «перед» и «после» первого главного знака (=знака импликации) формулы>
С учетом этой стратегии, ранее введенная эвристика может быть названа тактикой сечения 1+ (или тактикой сечения 1 по аксиоме +103), поскольку при введении формулы сечения мы редуцируем исходную задачу (|— A É С) к двум подзадачам следующего типа: j1: |— A É В и j2: |— A É [В É С] (заметим, что в данном случае мы вместо подзадачи j2 типа |— В É С, которая требует своего решения по правилу сечения, должны решить более «слабую» задачу |— A É [В É С]).
Снова обратимся к примерам из книги А. Черча, с целью прояснения «смысла» построения вывода (после завершения вывода дадим оригинальный фрагмент из Черча).
Задача 122: |— f É р. В соответствии с тактикой сечения по аксиоме +103, редуцируем исходную задачу |— f É р к двум подзадачам: j1: |— f É X и j2: |— X É p.
<Введем еще одну поисковую тактику (эвристику): при решении задач с f необходимо использовать аксиому +104>
Если воспользоваться вышеприведенной тактикой, то задача j2: |— X É p может быть решена при отождествлении X @ p É f É f (с антецедентом +104), т.к. в этом случае j2: |— X É p решается как аксиома +104. Соответственно, j1: |— f É X (с учетом отождествления X @ p É f É f) решается как вариант +102 ([f É. [[p É f] É f]].
Поиск вывода завершен и теперь — с учетом найденной в ходе поиска «схемы» решения — построим вывод |— f É р <с анализом>:
1. +103
2. подстановка в <1> s/f, p/pÉfÉf, q/f: [f É pffp] É [[f É [pf É f]] É [f É p]]]
3. +102
4. подстановка в <3> p/pffp, q/f: pffp É [f É pffp]
5. +104
6. f É pffp из 4, 5 по modus ponens
7. [f É [pf É f]] É [f É p] из 2, 6 по modus ponens
8. подстановка в <3> p/f, q/pf: f É [pf É f]
9. f É p из 7, 8 по modus ponens
=== теорема доказана ===
~~~~~~~~~~~~~~~~~~~~~
+122 f É р
Одновременной подстановкой в +102: |— p É f É f É p É < f É < p É f É f É p
В силу +104 и по модус поненс: |— f É < p É f É f É p
Одновременной подстановкой в +103: |— f É [p É f É f É p] É< f É [p É f É f] É< f É p
По модус поненс: |— f É [p É f É f] É < f É p
Одновременной подстановкой в +102: |— f É < p É f É f.
Наконец, по модус поненс: |— f É p
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Задача 123: |— pf É pq. При решении данной задачи — с учетом более «богатой» структуры формулы pf É pq — будем использовать стратегию поиска, отличную от стратегии сечения.
***
В общем плане эта стратегия заключается в сведении решения искомой задачи к решению другой подзадачи. (При этом временные метапеременные нам могут не потребоваться, т.к. структура искомой формулы (иногда) полностью определяет структуру формулы подзадачи, т.е. это стратегия более проста по сравнению с стратегией сечения. В этом случае эта стратегия, вслед за Смальяном, в общем плане может быть также названа аналитическим сечением).
Однако в данном случае применяемая нами тактика — эвристика 1 — еще более проста, поскольку даже (аналитическим) сечением не является, т.к. вид (структура формулы) подзадачи полностью определяется структурой (формулы) исходной задачи. Тактика поиска вывода данной эвристики основана на анализе структуры искомой формулы и обнаружении ее сходства с «длинным хвостом» аксиомы +103:
Если искомая формула имеет вид Ax É Ay (т.е. имеет вид сложной импликации, начинающейся с одинаковых антецедентов A ), то можно перейти к решению подзадачи типа |— A É хy <в этом случае подзадача является антецедентом варианта аксиомы +103 ([A É хy] É [Ax É Ay]), а сама задача — ее консеквентом, поэтому решив подзадачу и применив правило модус поненс, мы решим и задачу>.
Намеченную нами стратегию и эвристику 1 как конкретизацию стратегии сечения (+ эвристики 2 и 3 — см. ниже) можно рассматривать как вырожденный случай правила сечения — стратегию сечения 0, или как применение правила сечения не «внутри» выводимой формулы, а «перед» ней. Данная тактика может быть сформулирована так:
Если есть формула С, то вместо ее доказательства можно перейти к решению подзадачи j1: |— A É C, при условии, что решена (под)задача j2: |— A.
Т.е. здесь (также как и в стратегии сечения 1) исходная задача |— С редуцируется к решению двух подзадач: |— A É C и |— А и по модус поненс получаем исходную формулу С.
***
С учетом эвристики 1 тактика — «схема» — решения |— 123 такова. Для решения |— pf É pq достаточно решить |— p É fq, а эта подзадача решается с использованием |— 122, т.к. консеквент подзадачи (f É q) является вариантом |—122 и по тактике, связанной с аксиомой +102, подзадача решается. Поиск вывода завершен и теперь, используя найденную «схему» решения, построим вывод <с анализом>:
1. +103
2. подстановка в <1> s/p, p/f, q/q: [p É fq] É [pf É pq]
3. 122
4. подстановка в <3> f/f, p/q: f É q
5. +102
6. подстановка в <5> p/+122, q/p: 122 É [p É 122]
7. p É fq из 6, 3 по modus ponens
8. pf É pq из 2, 7 по modus ponens
=== теорема доказана ===
~~~~~~~~~~~~~~~~~~~~~
+123 p É f É < p É q
Одновременной подстановкой в +102: |— f É q É < p É < f É q
Подстановкой в +122: |— f É q
По модус поненс: |— p É < f É q
Одновременной подстановкой в +103: |— p É [f É q] É < p É f É < p É q
Наконец, по модус поненс: |— p É f É < p É q
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Сформулируем еще две эвристики, связанные уже не с +103, а теоремами из задач 12.3 и 12.4 < гипотеза: этот набор эвристик является исчерпывающим для решения задач!>.
Эвристика 2 является более сильным «вариантом» эвристики 1 и связана с теоремой |— qr É< pq É pr. Заметим, что «хвост» этой теоремы содержит две формулы, начинающихся с одинакового антецедента, поэтому задачу |— pq É pr можно свести к решению подзадачи |— qr. Эвристика 2 является тактикой стратегии аналитического сечения:
Если искомая формула имеет вид Ax É Ay (т.е. имеет вид сложной импликации, начинающейся с одинаковых антецедентов A ), то можно перейти к решению подзадачи типа |— хy <в этом случае подзадача является антецедентом варианта теоремы 12.3 ([xy] É [Ax É Ay]), а сама задача — ее консеквентом, поэтому решив подзадачу и применив правило модус поненс, мы решим и задачу>.
Эвристика 3 основана на теореме 12.4 (|— pq É< qr É pr.) и в этом отношении принципиально отличается от эвристик 1 и 2. Она применяется в случае, если «вид» доказываемой формулы является сложной импликацией, у которой одинаковы консеквенты (а не антецеденты, как в случае эвристик 1 и 2). Поэтому подзадача в этом случае формулируется как |— pq. С другой стороны, эвристика 3, также как и эвристика 2, более проста чем эвристика 1 и является тактикой стратегии аналитического сечения:
Если искомая формула имеет вид xA É yA (т.е. имеет вид сложной импликации, c одинаковыми консеквентами A ), то можно перейти к решению подзадачи типа |— yx <в этом случае подзадача является антецедентом варианта теоремы 12.4 (|— [yx] É [xA É yA]), а сама задача — ее консеквентом>.
<Заметим, что «прямое» использование теоремы 12.4, т.е. ее «прочтение» слева направо соответствует правилу сечения; поэтому, отнюдь не случайно, что в модифицированном варианте исчисления Рw Черч включает именно эту теорему в число исходных аксиом как альтернативу аксиоме +103.>
***
Для обоснования эвристик 2 и 3 докажем (соответственно, без использования эвристики 2 и эвристики 3) теоремы 12.3. и 12.4. Вместе с тем, еще раз продемонстрируем «механизм» решения задач в исчислении Р1.
Задача +12.3: |— qr É< pq É pr. В соответствии с тактикой сечения по +103 (и общей эвристикой), редуцируем исходную задачу к двум подзадачам: j1: |— qr É X и j2: |— X É [pq É pr]. Заметим, что j2 может быть решена, если X соответствует антецеденту +103, т.е. если X @ p É qr, так как в этом случае j2 является вариантом +103 (p É qr É< pq É pr); а при этом отождествлении X решена и задача j1 как вариант +102 (qr É [p É qr]). Поиск вывода завершен и теперь построим вывод 12.3 <с анализом>:
1. +103
2. подст. в <1> s/qr, p/pÉqr, q/pqÉpr: qr É [p É qr É<pq É pr] É< qr É<p É qr É<12.3
3. подст. в <1> s/p, p/q, q/r: p É qr É< pq É pr
4. +102
5. подст. в <4> p/pÉqrÉ<pqÉpr, q/qr: [p É qr É< pq É pr] É [qr É [p É qr É< pq É pr]]
6. qr É [p É qr É< pq É pr] из 5, 3 по modus ponens
7. qr É [p É qr] É< 12.3 из 2, 6 по modus ponens
8. подст. в <4> p/qr, q/p: qr É [p É qr]
9. 12.3 < т.е. qr É< pq É pr> из 7, 8 по modus ponens
=== теорема доказана ===
Задача +12.4: |— pq É< qr É pr. В соответствии с тактикой сечения по +103 (и общей эвристикой), редуцируем исходную задачу к двум подзадачам: j1: |— pq É X и j2: |— X É [qr É pr]. Заметим, что j1 будет решена как вариант +102, если X @ Y É pq. С учетом этого отождествления Х подзадача j2 такова: |— [Y É pq] É [qr É pr]. Если, в свою очередь, произвести отождествление Y @ qr, то к задаче j2 ([qr É pq] É [qr É pr]) можно применить эвристику 1, т.е. свести решение подзадачи j2 к (под)подзадаче j3: |— [qr É< pq É< pr], а она есть ни что иное как теорема 12.3. (т.е. j3 решена). Поиск вывода завершен, а временные (мета)переменные получили следующие значения: Y @ qr; X @ qr É pq. Перейдем к построению вывода <с анализом>:
1. +103
2. подст. в <1> s/pq, p/qrÉpq, q/qrÉpr: pq É [qrÉpq É<qr É pr] É< pq É [qrÉpq] É<12.4
3. подст. в <1> s/qr, p/pq, q/pr: [ qr É [pq É qr]] É<qrÉpq É<qrÉpr
4. 12.3
5. qr É pq É< qr É pr из 3, 4 по modus ponens
6. +102
7. подст. в <6> p/qrÉpqÉ<qrÉpr, q/pq: [qr É pq É< qr É pr] É [pq É [qr É pq É< qr É pr]]
8. pq É [qr É pq É< pq É pr] из 7, 5 по modus ponens
9. pq É [qr É pq] É< 12.4 из 2, 8 по modus ponens
10. подст. в <4> p/pq, q/qr: pq É [qr É pq]
11. 12.4 < т.е. pq É< qr É pr> из 9, 10 по modus ponens
=== теорема доказана ===
***
Различные тактики сечения и другие метатеоремы
В заключении этой части сформулируем еще несколько тактик сечения. Во-первых, это тактика поиска вывода, связанную с правилом сечения 2. Ее суть заключается в том, что имея сложную импликацию, мы можем «вставлять» формулу сечения не только «впереди» формулы (тактика сечения 0) и «около» главной импликации формулы (тактика сечения 1), но и «около» вспомогательной (второй) импликации формулы. Точная формулировка этой тактики такова:
Если выводимая формула имеет вид A É [B É C], то вместо ее решения (вывода) можно перейти к решению двух подзадач: j1: |— B É D и j2: |— D É C.
По индукции (у нас уже есть тактика сечения 0 и 1) можно тактику сечения 2 обобщить следующим образом (обобщенная тактика сечения вправо):
Если выводимая формула V имеет вид V @ A1 É< A2 É<… É< An, то вместо ее решения (вывода) можно, произведя «сечение» в последней (любой —??) импликации формулы V по некоторой формуле сечения Bj, перейти к решению двух подзадач: j1: |— An-1 (Aт) É Bj и j2: |— Bj É An (Am+1)
Т.е. можно проводить «сечение» в самой «правой» (или любой —??) импликации формулы, вставляя формулу сечения вместо («около») этой импликации, и редуцируя решения исходной задачи к решению двух подзадач. Этот результат интуитивно очевиден, но не доказан (идея доказательства заключается в том, что по правилу сечения 1 из j1: |— An-1 É Bj и j2: |— Bj É An вытекает выводимость |— An-1 É An (см. доказательство этого факта ниже), а если выводима формула |— An-1 É An, то выводима и любая (более слабая формула) |— A1 É< A2 É<… É< An-2 É< An-1 É An по аксиоме +102, которая при многократном применении позволяет навешивать какое угодно количество антецедентов к доказанной формуле (теореме) |— An-1 É An)
Более проблематичным представляется обобщение правила сечения (1) по любой импликации вправо (для формул вида A1 É< A2 É<… É< An) и по (2) импликации влево (для формул вида A1 É A2 É… É An). === задача для сам. работы! ===
В заключении приведем точное обоснование правил сечения 0 и 1. Т.е. докажем следующие метатеоремы (леммы):
Метатеорема (сечения) 1: Из |— A É B, |— B É C следует |— A É C.
Доказательство:
1. A É B
2. B É C
3. + 103
4. подст. <3> s / A, p / B, q / C: A É [B É C] É< A É B É< A É C
(заметим, что B É C и A É B в выводе имеются: см. шаги 1 и 2)
5. +102
6. подст. <5> p / BÉC, q / A: BÉC É< A É< B É C
7. A É< B É C из 6, 2 по модус поненс
8. A É B É< A É C из 4, 7 по модус поненс
9. A É C из 8, 1 по модус поненс
=== метатеорема доказана ===
Метатеорема (сечения) 2: Из |— A, |— A É B следует |— B.
Доказательство (тривиально!):
1. A É B
2. A
3. B из 2, 1 по модус поненс
=== метатеорема доказана ===
Метатеорема 3: Из |— A следует |— B É A.
(тактика навешивания антецедентов слева: по индукции можно доказать корректность последующих — многократных — навешиваний антецедентов слева; при этом каждая последующая формула (с дополнительным антецедентом) будет являться все более «слабой»)
Доказательство:
1. A
2. +102
3. подст. <2> p / A, q / B: A É< B É A
4. B É A из 3, 1 по модус поненс
=== метатеорема доказана ===
Метатеорема 4: Из |— AÉ < B É С следует |— B É < A É С.
(тактика перестановок антецедентов: идея взята из 12.7.3 (закон коммутации))
Доказательство:
1. A É [B É C]
2. + 103
3. подст. <3> s / A, p / B, q / C: A É [BÉC] É< AÉB É< AÉC
4. A É B É< A É C из 3, 1 по модус поненс
5. 12.4 <закон транзитивности импликации>
6. подст. <5> p / B, q / AB, r / AC: B É AB É< AB É AC É< B É AC
7. +102
8. подст. <7> p / B, q / A: B É AB
9. AB É AC É< B É AC из 6, 8 по модус поненс
10. B É< A É C из 9, 4 по модус поненс
=== метатеорема доказана ===
***