<<
>>

Глава 2. Анализ системы натурального вывода BMV

Формулы, определяемые пунктом 1, называются элементарными формулами. Все остальные формулы называются сложными формулами.

Буквами А, В, С,... (с индексами и без них) обозначаются произвольные формулы.

Зададим несколько стандартных определений, необходимых для

формулировки правил исчисления.

В выражениях ναΛ и 3аА формула А называется областью действия кванторов V и 3, взятых по индивидной переменной α.

Вхождение индивидной переменной α называется связанным, если α расположена непосредственно справа от квантора или α находится в области действия квантора, взятого по α. Остальные вхождения α называются свободными. Индивидная переменная α является свободной (связанной) в формуле А, если она имеет хотя бы одно свободное (связанное) вхождение в формуле А.

Вхождение квантора в выражениях VαА и 3αА называется вырожденным, если ни одно вхождение переменной α не находится в А. Например, вхождение V в формулу Vx3yP(y) вырождено. Если некоторое вхождение переменной α в А связано двумя или более вхождениями кванторов по α, то все эти вхождения кванторов по α, кроме самого правого, являются вырожденными [Непейвода, с. 184]. Например, вхождение V в формулу Vx3хP(х) вырождено.

Пусть t - терм, α - индивидная переменная. Тогда выражение вида А(оЛ) обозначает результат подстановки в формулу Λ(α) вместо всех свободных вхождений α терма t. Подстановка A(α∕t) считается правильной, если никакое свободное вхождение α не лежит в области действия никакого квантора по каждой переменной, входящей в терм t.

Частным случаем выражения А^/t) является выражение A(α∕β), обозначающее правильную подстановку в А переменной β вместо переменной α.

При этом фиксируется множество всех свободных переменных γι,., γnв А и β ∉{γi,., γn}. Данное выражение обозначается как A(α∕β, γ1,..., γn).

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

введения и исключения кванторов называются кванторными правилами. Полужирным начертанием в формулировке некоторых правил выделена большая посылка.

Задаются следующие правила системы BMV (BMV-правила):

В правилах ⊃bи —в формула С является последней неисключенной посылкой (это понятие будет разъяснено ниже). А(оЛ) и A(α∕β) - результаты правильной подстановки.

В правилах Vbи 3и запись «β - абс.; γ1,..., γn- огр.» означает, что β абсолютно ограничена в выводе и переменная β относительно ограничивает в выводе каждую переменную из множества γ1,..., γn, где {γ1,..., γn} - это множество всех свободных переменных, входящих в посылки данных правил.

В дальнейшем мы иногда вместо «β относительно ограничена в выводе» будем писать «β ограничена», не указывая на ту переменную, которая относительно ограничивает β, а вместо «β абсолютно ограничена в выводе» - «β абсолютна». Переменные, не ограниченные абсолютно в выводе, будут называться неабсолютными. Содержательный смысл понятий «абсолютно ограниченная переменная» и «относительно ограниченная переменная» см. [Бочаров и Маркин, с. 133-134].

Определение 2.1.3.Выводом в системе BMV (ВМV-выводом) называется непустая конечная последовательность формул С1, C2,., Cn (n ≥ 1), удовлетворяющая следующим условиям:

1.

каждая формула есть либо посылка, либо получена из предыдущих по одному из BMV-правил;

2. при применении правил ⊃bи — в все формулы, начиная с последней неисключенной посылки Сі(1 ≥ i ≥ n) и вплоть до результата применения данного правила Ci⊃Cj (1 ≥ j ≥ n) или — Сі,исключаются из дальнейших шагов вывода в том смысле, что к ним запрещено применять правила вывода;

3. ни одна индивидная переменная в выводе не ограничивается абсолютно более одного раза;1

4. ни одна переменная не ограничивает в выводе сама себя.

Выводом формулы В из непустого множества посылок Г называется BMV- вывод, в котором множество неисключенных посылок есть Г и последняя формула есть формула В.

Доказательством формулы В называется BMV-вывод формулы В из пустого множества неисключенных посылок.

Теоремой называется формула, для которой имеется доказательство.

Определение 2.1.4.Завершенным ВМV-выводом называется ВМV-вывод, в котором никакая переменная, абсолютно ограниченная в выводе, не встречается свободно ни в неисключенных посылках, ни в заключении. Завершенное доказательство есть завершенный ВМV-вывод из пустого множества неисключенных посылок.

Проанализируем правила системы.

Правила для конъюнкции, а также правило введения дизъюнкции, обычны для систем натурального вывода: их можно обнаружить в [Генцен].

Что касается правила для исключения дизъюнкции, то иногда его формулируют в виде правила разбора случаев (р.с.): из A V B, A ⊃C, B ⊃C следует C. Известно, что р.с. сильнее, чем vuв том смысле, что, например, в интуиционистской логике можно

показать с помощью р.с. производность vh,но невозможно показать с помощью vu производность р.с.. Однако существуют определенные трудности с построением процедуры поиска натурального вывода типа Куайна с правилом р.с. [Макаров].

Что касается правила введения импликации, то специфика этого правила в том, что формула С является последней неисключенной посылкой.

Данное требование необходимо для корректности системы. При применении этого правила выводима формула С ⊃В и из вывода исключаются все формулы, начиная с формулы С и заканчивая формулой, непосредственно предшествующей формуле С ⊃В. Формула исключается из вывода не в том смысле, что она стирается и удаляется, а в том смысле, что к данной формуле не может быть применено ни одно правило вывода.

Наличие правила ⊃u- чуть ли не обязательное свойство всех систем натурального вывода.

Правило —и (снятие двойного отрицания) стандартно.

Что касается правила введения отрицания, то иногда используют два правила: из В, —В следует ⊥и из ⊥следует С, где ⊥- знак противоречия (тождественно ложной формулы) и С - произвольная формула. В нашей системе формула С не произвольна: она является последней неисключенной посылкой, что, опять же, обусловлено требованием корректности системы. Применение этого правила также влечет исключение из вывода всех формул, начиная с формулы С и заканчивая формулой, непосредственно предшествующей формуле —С.

Кванторные правила исключения квантора общности и введения квантора существования обычны. Специфика нашей системы - в формулировке правила введения квантора общности и правила исключения квантора существования.

Пусть 3yP(y) - формула, причем P - одноместный предикатор. Можно, например, не нарушая требования правильной подстановки, получить из 3yP(y) по 3и формулу P(x), затем применить Vbи получить VyP(y). Из VyP(y) с помощью правил Vu, 3в можно снова получить 3yP(y) и т.д.

Отметим, что в системе BMV такие бесконечные преобразования формул ограничиваются понятием вывода. Однако нам важен тот факт, что такие

1 Иногда пишут «не может абсолютно ограничиваться дважды». При этом Е.К. Войшвилло отмечал, что данное требование можно нарушить без ущерба для корректности, «когда правило Vbили 3ивторично применяется для вывода из той же формулы» [Войшвилло, с. 90-91].

преобразования возможны, если не следовать понятию вывода, а следовать только формулировкам Vb,3и и требованию правильной подстановки.

Иногда формулировки данных правил не позволяют такие взаимопревращения формул [Войшвилло]. Более того, Дж. Пеллетье вообще не формулирует правила введения квантора общности явным образом. Аналог этого правила имплицитно содержится в формулировке достижимости некоторого подвывода [Pelletier].

Необходимость учета абсолютных и ограниченных переменных обусловлена, как мы далее увидим, требованием, чтобы ни одна переменная не ограничивала в выводе сама себя.

У. Куайн, например, явно указывает на наличие абсолютно ограниченных (flagged) переменных и не указывает явно на наличие относительно ограниченных переменных. Однако он задает свободные переменные в алфавитном порядке и требует, чтобы при применении правил 3и, Vbновая свободная переменная не предшествовала в алфавитном порядке имеющимся в формуле свободным переменным [Quine]. Именно таким образом У. Куайн избегает самоограничения переменной.

Касаясь правил вывода нашего исчисления в целом, отметим их симметричность: каждой логической связке соответствуют хотя бы одно правило исключения и хотя бы одно правило введения. Свойство симметричности правил натурального вывода идет от работ Г. Генцена [Генцен]. См. также [Fitch]. В то же время симметричность правил не является необходимым свойством натурального вывода. Можно указать на системы натурального вывода, где данное свойство не выполняется [Pelletier].

Проанализируем понятие вывода в системе.

Требование, чтобы в правилах ⊃b, —в формула С была последней

неисключенной посылкой, обосновывается следующим образом:

В данном выводе мы от вывода формулы С из посылок A, B по правилу ⊃b перешли к доказательству формулы A ⊃C. Однако такой переход семантически неверен, т.е. из A, B |= C не следует |= A ⊃C.

Аналогично обосновывается данное требование в формулировке правила —в.

Обоснование требования не ограничивать абсолютно некоторую переменную более одного раза, а также требований наличия завершенного вывода, можно найти в [Quine, стр. 97-99].

Что касается запрета на самоограничение переменной, которого нет в [Quine], то он обосновывается, например, невозможностью построения завершенного вывода 3xVyA(x, y) из Vy3xA(x, y) [Бочаров и Маркин, с. 136].

Необходимость введения понятия завершенного вывода (доказательства), наряду с понятием вывода (доказательства), является характерным свойством выводов в первопорядковых натуральных исчислениях типа Куайна, где в общем случае заключение не следует из своих посылок: «При незавершенности вывода не обеспечена истинность заключения при истинности посылок» [Войшвилло, с. 94].

Натуральные исчисления типа Куайна [Quine], [Войшвилло], [Бочаров и Маркин], [Ивлев] противопоставляются натуральным исчислениям типа Генцена [Генцен], [Fitch], [Li], не требующим введения понятия завершенного вывода.

В качестве примеров приведем завершенный BMV-вывод —3xP(x) |- Vx— P(x).

Помещаем формулу —,3xP(x) в качестве посылки. Берем другую посылку P(x).

Применяя к этой формуле правило 3в, выводим формулу 3xP(x). Поскольку формула

—3xP(x) (шаг 1) противоречит формуле 3xP(x) (шаг 3), на шаге 4 выводим формулу

—P(x), применяя правило —в. Формула —P(x) является отрицанием последней неисключенной посылки P(x). При этом все формулы, начиная с формулы P(x) и заканчивая формулой 3xP(x), исключаются из дальнейших шагов вывода. Применяя к формуле —P(x) правило Vb,выводим формулу Vx—P(x). При этом переменная х является абсолютно ограниченной в выводе.

Данная последовательность формул является завершенным выводом формулы Vx—P(x) из посылки —3xP(x), поскольку она является выводом формулы Vx—P(x) из посылки —3xP(x) и абсолютно ограниченная переменная х не входит свободно ни в Vx—P(x), ни в —3xP(x).

<< | >>
Источник: ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ. АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ. Диссертация на соискание ученой степени кандидата философских наук. Москва - 2004. 2004

Еще по теме Глава 2. Анализ системы натурального вывода BMV:

  1. ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ. АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ. Диссертация на соискание ученой степени кандидата философских наук. Москва - 2004, 2004
  2. Глава 1. Феноменологический анализ воли
  3. Анализ космологических фрагментов Филолая
  4. 3. Историческое появление логики и теории зла: сравнительный анализ с идеями ранних пифагорейцев
  5. ГЛАВА I Псевдопифагорика
  6. Глава 3. Эстетизация воли в художественной литературе
  7. Глава 2. Потенциал эстетизации в трактовках воли
  8. Глава 4. Проблема эстетизации воли в современной философии
  9. ГЛАВА II Трактат Тимея Локрского «О ПРИРОДЕ КОСМОСА И ДУШИ»
  10. Глава 3. самопознание и восхождение души в комментарии ПРОКЛА НА «ПЕРВЫЙ АЛКИВИАД»
  11. Оглавление