Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2



страница4/5
Дата02.01.2013
Размер0.5 Mb.
ТипДокументы
1   2   3   4   5
§ 2. Исчисление NK.
"Если к исчислению NJ присоединить "закон исключенного третьего" (tertium non datur), то получится полное классическое исчисление NK . Иными словами, кроме допущений, в качестве исходных формул вывода разрешается теперь брать "основные формулы" вида АА, где А–произвольная формула.

Таким образом, мы совершенно внешним образом предоставляем "закону исключенного третьего" особое место, так как мы считаем такую формулировку наиболее естественной. Можно было бы вместо схемы АА допустить новую схему фигуры заключения, а именно – фигуру заключения "Удаление двойного отрицания" (аналогично тому, как это сделано Гильбертом и Гейтингом). Однако эта фигура заключения выпадает из рамок NJ-фигур заключения, так как представляет собой новое удаление отрицания, допустимость которого никак не следует из способа введения знака отрицания" (Генцен Г. Исследования логических выводов. Математическая теория логического вывода М.1967г.).

Итак: переход от исчисления NJ к исчислению NK согласно Генцену возможен двумя способами:

а) NKtnd=NJ + ();

b) NKdn=NJ + ;

где выражение NKtnd означает, что натуральное классическое исчисление образовано из NJ-исчисления добавлением закона tertium non datur, а выражение NKdn означает, что натуральное классическое исчисление образовано из NJ-исчисления добавлением фигуры заключения exception of double negation (удаление двойного отрицания).
Определение NKtnd-вывода и NKdn-вывода совпадает с определением NJ-вывода. Однако в описание процедуры поиска вывода внесем изменения.

Для NKtnd- исчисления в пункте 5 выделим два шага:

а) если указанного списка допущений недостаточно для выведения "пограничной" формулы, то ищем "встроенный" вывод и, в случае успеха, восстанавливаем вывод в целом.

б) если применение пунктов 2–5а) не приводит к получению "пограничной" формулы, то к уже известным допущениям присоединим основную формулу вида AA и допущения вида и , где i и (i + 1) обозначают номера допущений и ; и в случае успеха восстанавливаем вывод в целом.

Заметим, что основная формула АА допущением не является и поэтому процедура отбрасывания допущений к ней не применяется.

Для NKdn-исчисления пункт 5 будет иметь вид:

а) Если указанного списка допущений недостаточно для выведения "пограничной" формулы, то ищем "встроенный" вывод и, в случае успеха, восстанавливаем вывод в целом.
б) если применение пунктов 2–5а) не приводит к получению "пограничной" формулы, то к уже известным допущениям добавляем формулу противоречащую консеквенту конечной формулы ("пограничной" формуле предполагаемого вывода), т.е. если консеквент имеет вид А, добавляем к допущениям формулу вида А, а если консеквент имеет вид А, добавляем формулу вида А.
Тогда косвенный вывод в NKdn-исчислении будет иметь еще одну дополнительную схему по отношению к NJ-исчислению:



***
Сравним поиск вывода для NJ и NK исчислений на примере одной формулы, известной как формула Пирса: (((рq)p)p).
Пример 11.

Вывод формулы (((pq)p)p) в NJ-исчислении построить невозможно. 11.1.Действительно, после первого шага предполагаемый вывод имеет вид:


Анализируем создавшуюся ситуацию. "Пограничная" формула р не содержит логических знаков, в частности, знака отрицания, а единственное допущение не содержит в качестве главного знака ни знака  ни знака , следовательно, мы не можем ввести в вывод дополнительные допущения согласно пунктам 2 и 3 процедуры для NJ-исчисления.

Попробуем применить пункт 5 указанной процедуры, т.е. попытаемся найти "встроенный" вывод. "Пограничную" формулу р мы могли бы получить из формулы (pq)p если бы существовала возможность обосновать использование в нашем выводе формулы pq, т.е. вывод мог бы иметь вид:

.
Рассмотрим следующую часть вывода:

.

Формула pq должна быть конечной формулой некоторого вывода надстроенного над ней. Здесь возможно несколько вариантов, например:

11.1.1 пусть последний шаг интересующего нас вывода – это введение импликации:

,

Далее замечаем, что получить формулу q непосредственно из формулы p невозможно, поскольку нет фигуры заключения, позволяющей сделать такой вывод. Следовательно, так как формулы q и p не содержат логических знаков, мы должны вновь использовать встроенный вывод некоторой формулы, с помощью которой и формулы р мы могли бы получить формулу q. Это могла бы быть формула pq, если бы она была конечной формулой (т.е. формулой, не зависящей ни от каких допущений) некоторого вывода. Тогда вывод имел бы вид:
,

но формула pq именно та, вывод которой мы пытаемся построить. Следовательно, формула pq может быть только подформулой формулы, применение которой, в свою очередь, необходимо обосновать с помощью "встроенного" вывода. Структуру предполагаемой формулы можно представить в трех вариантах:

11.1.11) как формулу, которая вместе с уже известным допущением (формулой р) позволит нам вывести формулу pq, например, такой формулой может быть формула p(pq). В этом случае вывод будет иметь вид:

.

Теперь нам необходимо обосновать использование формулы p(pq).

После двукратного обратного применения фигуры заключения + приходим к ситуации:

,
которая, по сути, совпадает с ситуацией, обозначенной нами пунктом 11.1.1.; т.е. происходит итерация допущения р.

11.1.12) как формулу, которая выводима в NJ-исчислении и содержит формулу pq в качестве подформулы, но получение формулы pq из искомой формулы потребует введения в основной вывод нового допущения, отличного от уже известного допущения р:

,

мы видим, что в данной части основного вывода, заканчивающейся формулой pq, отброшены допущения, обозначенные номерами +3,+4 и +1, а допущение +2 (формула p) не отброшено. Следовательно, формула pq все еще зависит от данного допущения. Для завершения этой части вывода нам необходимо обосновать использование допущения р, но это невозможно в силу пунктов 2 и 3 процедуры для NJ-вывода. Следовательно, этот путь закрыт.

11.1.13) как формулу, которая содержит формулу pq, причем искомая формула будет, например, иметь вид АВ, где А- это формула, выводимая в NJ-исчислении, а В - это формула pq. Пусть например, это будет формула (pp)(pq). Тогда рассматриваемая часть вывода будет иметь вид:

.

Теперь, если формула (pp)(pq) NJ-выводима, то мы сможем завершить вывод в целом. Попробуем это осуществить:

.
Увы, мы опять сталкиваемся с необходимостью обосновать переход от p к q. т.е. имеем такую часть вывода , которая оказалась непреодолимым препятствием при разборе предыдущих случаев.

Таким образом, случай 11.1. не приводит нас к разрешению поставленной задачи: ввести в доказательство формулы (((pq)p)p) встроенный вывод, обосновывающий использование формулы pq. Следовательно, необходимо рассмотреть другие возможные случаи.
11.2. Итак, мы рассматривали следующую исходную ситуацию :


и для случая 11.1. предположили, что формула pq может появиться в результате применения фигуры заключения +. Однако на этом пути мы потерпели неудачу. Следовательно, нам остается предположить, что эту формулу можно было бы получить по одной из фигур заключения для пропозициональных связок. Но и этот путь невозможен. Действительно, в нашем исчислении существуют только две фигуры заключения, применение которых позволяет отбрасывать все допущения, а именно: + и +. Мы уже убедились, что применение фигуры + не приводит к желаемому результату. Применение фигуры + также невозможно, поскольку формула pq в качестве главного знака формулы содержит знак импликации, а не знак отрицания. Все остальные фигуры ставят заключительную формулу в зависимость от допущений, соответствующих этим фигурам, а обоснование указанных допущений, без применения фигур + и +, требует введения встроенных выводов, построение которых (а скорее невозможность построения) будет сводиться в конечном результате к случаю 11.1.

Таким образом, относительно формулы (((pq)p)p) мы можем сказать следующее: все предпринятые нами попытки построить вывод данной формулы в исчислении NJ закончились неудачей, и, по-видимому, данная формула не выводима в исчислении NJ.

Безусловно, утверждение о не выводимости указанной формулы оставляет нас в сомнении относительно самого этого утверждения, а также относительно целесообразности использования исчисления NJ для поиска вывода заданных формул. Однако эту тему мы обсудим позднее, а именно после рассмотрения доказательства формулы Пирса для натуральных классических исчислений.
Пример 12. Требуется доказать формулу Пирса (((pq)p)p) в исчислении NKtnd. Напомним, что исчисление NKtnd получается из исчисления NJ добавлением к фигурам заключения этого исчисления основной формулы вида АА.

1) Итак, исходный шаг имеет вид:

.
2) Тогда на предыдущем шаге вывод имел вид:



  1. На втором шаге мы выявили единственное допущение: (pq)p, и как уже нам известно, из примера 11 следует, что этого допущения нам недостаточно для доказательства данной формулы. Поэтому теперь мы будем использовать пункт 5б процедуры для NKtnd-исчисления, т.е. введем в вывод основную формулу вида АА. Для нашего случая это будет формула рр:

.


  1. Заметим, что формула рр не является допущением. Это означает, что при завершении вывода данную формулу мы не должны отбрасывать, но тем не менее, использование в выводе основной формулы позволяет нам вводить новые допущения, а именно допущения: р и р. Далее, поскольку основная формула содержит в качестве главного знака знак , то одной из фигур заключения, применяемых в выводе, будет фигура заключения -. Таким образом, предполагаемый вывод будет иметь вид:

.


  1. Следующий шаг требует подробного объяснения. Заметим, что формулу р мы могли бы вывести из второго и третьего допущения, например:

.

Однако в этом случае формула р ни как не связана в выводе с допущением (pq)p, следовательно, нам необходимо искать другой путь. Это означает, что мы должны найти подходящий встроенный вывод.


  1. Приведем одну из возможных схем встроенного вывода:



Здесь формула p(pq) выводима в исчислении NKtnd, а допущения р и р, включенные в вывод благодаря введению основной формулы рр, отбрасываются посредством применения фигуры заключения -. Конъюнкция посылок обозначенных как +2 и +1 необходима для выполнения формального условия о существовании части вывода с использованием посылки +2. Мы могли бы написать просто посылку +2, но это не будет согласовываться с формой фигуры заключения -. Таким образом формула Пирса доказуема в исчислении NKtnd..
Пример 13. Требуется доказать формулу Пирса в исчислении NKdn. Напомним, что в этом случае мы будем использовать не основную формулу вида АА, а фигуру заключения "Удаление двойного отрицания".

  1. На исходном шаге предполагаемый вывод имеет вид:

.


  1. Следующий шаг это:




  1. На этом шаге мы используем фигуру заключения "Удаление двойного отрицания", что позволит нам ввести в вывод допущение p:




  1. Теперь рассуждаем следующим образом: использование допущений (pq)p и p должно привести нас к формуле Л, т.е. некоторый участок вывода должен иметь следующий вид:

.


  1. Для завершения части вывода:


необходимо ввести в доказательство встроенный вывод, так же как это было сделано в пункте 6 примера 12.




  1. Теперь соединяем все части вывода:



Вывод формулы p(pq) приведен нами в примере 11 пункт 11.1.12.

Итак, формула Пирса выводима и в исчислении NKdn.

***
Подведем итоги.
Натуральные исчисления обладают следующими достоинствами:

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

  2. выводы истинных формул в этих исчислениях почти всегда короче, чем в аксиоматических, это существенно связано с тем, что в аксиоматических выводах одна и та же формула в большинстве случаев появляется несколько раз (как часть других формул), тогда как в NJ- и NK- выводах это имеет место гораздо реже;

  3. имеет место заслуживающая внимания систематизация фигур заключения: с каждым из логических знаков &, , , , ,  связана одна фигура «введения» и одна фигура «удаления» его, как внешнего знака формулы;

  4. следствием систематизации фигур заключения является возможность эффективной проверки доказательств; каждый шаг вывода есть применение одной из фигур заключения и правильность шагов проверяется их сопоставлением со схемами соответствующих фигур заключения;

  5. определение вывода содержит точный критерий завершения доказательства истинных формул: отбрасывание всех допущений (независимость конечной формулы от допущений);


Однако, кроме достоинств, натуральные исчисления обладают и рядом формальных недостатков:


  1. для формул, не выводимых в этих исчислениях, нет точного критерия, указывающего на завершение поиска вывода (см. пример 11);

  2. в выводе доказываемой формулы могут участвовать формулы, не входящие в нее в качестве подформул (в примере 6 - это формула «Л»);

  3. следствием предыдущего недостатка является тот факт, что

доказательство формул может содержать «встроенные» выводы, которые существенно усложняют поиск вывода (см. примеры 11-13).

  1. вывод формул может содержать «сечения».


Термин «сечение» вводится нами в этой главе впервые. И хотя смысл и значение его станет вполне ясен только при изложении секвенциальных исчислений, уже в данном параграфе мы введем для него некоторые разъяснения.

Термин «сечение» обозначает последовательное применение в одной нити (см.стр.6) фигуры «введения» и «фигуры» удаления одного и того же логического знака. Так на станице 35 (пример 8) часть вывода



является сечением. Сечение усложняет вывод, так как мы, по сути, делаем лишние шаги: сначала вводим логический знак, а затем удаляем.

По-видимому, одной из главных причин указанных недостатков является наличие в натуральных исчислениях таких фигур заключения, в которых нижняя формула не содержит верхние формулы в качестве в качестве подформул. К ним относятся следующие фигуры &-, -, -, -, -, -, .

Действительно, по виду нижней формулы любой из указанных фигур, мы не можем определить: из каких допущений данная формула следует. В частности, она может следовать и из формул, полученных посредством «встроенного» вывода (см. пример 11).

Эта особенность натуральных исчислений превращает поиск вывода в них в, вообще говоря, неопределенную процедуру, и, следовательно, исчисления NJ и NK являются практически бесполезными в качестве разрешающих процедур, даже для логики высказываний.

Тем не менее, исследование натуральных исчислений позволяет сформулировать одно из важнейших требований, предъявляемых с точки зрения поиска вывода, к логическим исчислениям вообще, а именно: вывод в исчислении должен обладать свойством подформульности, это означает, что вывод конечной формулы должен содержать только те формулы, которые входят в конечную формулу в качестве подформул.

Преобразование натуральных исчислений в севенциальные позволяет осуществить переход к исчислениям, выполняющим это требование.

Рекомендованная литература:

  1. Генцен Г. Исследования логических выводов. Математическая теория логического вывода. М. 1967.

  2. Клини С.К. Введение в метаматематику. М. 1957.

  3. Клини С.К. Математическая логика. М. 1967.

  4. Серебрянников О.Ф. Эвристические принципы и логические исчисления. М. 1970.

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

  6. Prawitz D. Natural deduction. Stockholm. 1965.


Упражнения
1   2   3   4   5

Похожие:

Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconКлассическое определение вероятности. Комбинаторные методы решения задач
Цель: выработать умение решать задачи на определение классической вероятности с использованием основных формул комбинаторики
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconПриме Например, представим систему, которая состоит из трех подсистем. Соответственно, и требования могут быть разбиты на три части. Это можно представить в виде дерева следующим образом
Извлекаемые из документации требования представляются в виде дерева требований. Каждый узел-родитель в этом дереве является обобщением,...
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 icon2001 Дифференциальное исчисление функции одной переменной. Производная функции, ее геометрический и физический смысл. Определение
Определение. Производной функции f(x) в точке х = х0 называется предел отношения приращения функции в этой точке к приращению аргумента,...
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconПринципиальная схема сеточного метода решения детерминированного эквивалента стохастической задачи управления портфелем финансовых инструментов
Х переменных в динамике. Ключевая идея состоит в генерировании множества сценариев реализации случайных параметров в виде дерева...
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconОпределение и свойства предела последовательности. Определение
Определение: задать числовую последовательность – это значит сопоставить каждому номеру действительное число
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconРешение задач на вывод формул органических веществ. Алгоритм решения задач на вывод формул органических веществ
Обозначить формулу вещества с помощью индексов Х,у,z и т д по числу элементов в молекуле. Если продуктами горения являются со2 и...
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconУрок по теме «Функция квадратного корня»
В последствии появилось определение функции, данное Эйлером 1751 год, затем — у Лакруа в 1806 году — уже практически в современном...
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconА. Определение: множество неограниченно. Определение: последовательность удовлетворяет критерию Коши. Определение: последовательность не удовлетворяет критерию Коши. Определение точной верхней грани. Определение точной нижней грани

Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 icon«Определение степени с целым показателем»
Образовательная: дать определение дроби с целым показателем, научить представлять степень с целым отрицательным показателем в виде...
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 icon§ Определение доказуемой (выводимой) формулы
Следующим этапом в построении исчисления высказываний является выделение класса доказуемых (выводимых) формул
Разместите кнопку на своём сайте:
ru.convdocs.org


База данных защищена авторским правом ©ru.convdocs.org 2016
обратиться к администрации
ru.convdocs.org