Научная литература
booksshare.net -> Добавить материал -> Математика -> Манин Ю.И. -> "Доказуемое и недоказуемое " -> 19

Доказуемое и недоказуемое - Манин Ю.И.

Манин Ю.И. Доказуемое и недоказуемое — Советское радио , 1979. — 89 c.
Скачать (прямая ссылка): dokazuemoinedokazu1979.djvu
Предыдущая << 1 .. 13 14 15 16 17 18 < 19 > 20 21 22 23 24 25 .. 70 >> Следующая

43
ты е могут быть формулами L, истинность которых в стандартной интерпретации «угадана», — они называются специальными аксиомами L. (Примеры будут даны ниже в нп. 4.6—4.9.) Такие выводы рассматриваются как формальные эквиваленты математических доказательств (формулы Р—Рп исходя из посылок е). Имеются следующие основания для этого отождествления:
а) Как показано в п.3.3, если eCT^L для некоторой интерпретации <р и е|—Р, то PG T^L: из истинных формул выводятся только истинные же.
б) Была проделана большая экспериментальная работа по формализации математических доказательств, т. е. по замене их выводами в соответствующих языках класса 3?в частности Li Set. Констатировано, что для огромных фрагментов математики, включая основы теории целых и вещественных чисел, теории множеств и т. д., формализация доказательств в виде выводов в рамках 3?\ удается. В литературе по логике имеется много материала на эти тему (см., в 'частности, книгу Э. Мендельсона [2]).
в) Теорема Геделя о полноте логических средств 3?\ (см. § ‘6) показывает, что все формулы, истинные одновременно с s (во всех интерпретациях), выводимы из е.
Дальнейшее обсуждение ем. в «Отступлении о доказательстве».
Рассматриваются также выводы из множеств е другого типа. Например, можно исключить из е некоторые логические аксиомы, скажем, «Закон исключенного третьего» (В.1, и. 3.4) для формального исследования интуиционистских принципов. Или можно включать в е предположительно ложную формулу, с тем, чтобы вывести из е противоречие, рассуждая «от противного».
Продемонстрируем формальные аспекты противоречия:
4.2. Предложение.
Допустим, что е содержит все тавтологии типа В.2, п. 3.4. Тогда следующие два свойства е равносильны:
а) существует такая формула Р, что е |— Р и s \— ~] Р;
б) s (— Q для любой формулы Q.
Множество е с такими свойствами называется противоречивым.
Доказательство, б) г^а) очевидно. Наоборот, если г\—Р и з (— ДР, то, добавляя к описаниям этих выводов формулу }Р—* по предположению лежащую в е, и дважды применяя МР (к ней и |Р; к Р—«-Q и Р), получаем описание вывода Q из s.
4.3. Значительная часть теорем логики состоит в доказательстве утверждений вида „е [— Ри или „не г [- Ри для разных языков L, множеств s и (классов) формул Р.
Результат „е (— Ри может доказываться посредством предъявления описания вывода Р из е. Однако >в мало-мальски сложных случаях оно оказывается настолько длинным, что заменяется ии-
44
струкцией по составлению такого описания, более или менее полной. Наконец, доказательство «е| —Р» может вообще не сопровождаться предъявлением вывода Р из е, хотя бы и неполного. В этом случае мы «не доказываем Р, а доказываем, что существует доказательство Р» (см. пример в § 8 о расширениях языка).
Результат „не г|—Р“ в редких случаях может устанавливаться чисто синтаксическим рассуждением, но обычно доказательство опирается на конструкцию модели, т. е. интерпретации, в которой е истинно, а Р ложно (ср. обсуждение проблемы континуума в гл. III). Если „не е)—Р“ и „не е |— ДР“, формула Р называется независимой. от е.
Приведем два полезных элементарных результата о выводах. Видно, что по сравнению с обычными доказательствами выводы собраны из очень мелких деталей. Математик, как в семимильных сапогах, за один шаг покрывает целые поля формальных выводов.
4.4. Лемма.
Пусть е содержит тавтологии. Если е [— Р и е [— <3, то е [—
К Р А О-
Доказательство. Если Рь ..., Рт\ (2Ь ..., 0.п—выводы Р и <3 соответственно, то
Ог Р—«2—(РАО)), <2-(РД0), РАО
есть вывод РАО-- Третья от конца формула — тавтология, вторая от конца непосредственно следует по МР из нее и Рт=Р, последняя — по МР ИЗ второй И <2п='<3.
4.5. Лемма о дедукции.
Пусть г ~П> Ах I и Р — замкнутая формула. Если г у {Р} [— (3, то & [— Р —* С2-
Доказательство. Пусть — вывод <3 из г у {Р}.
Индукцией по п покажем, что существует вывод Р—'-0. из г.
а) п— 1. Тогда либо Оее, либо С} — Р. В первом случае Р-+-0. выводится по МР из С? и тавтологии &~*-(Р->-С)), во втором случае Р-уР есть тавтология.
б) п 5з 2. Предположим, что для выводов длины < п — 1 лемма доказана. Тогда е [— Р—^ для всех /<я—1. Далее, для 0п = 0 имеются следующие возможности:
61) ?)ее; б2) 0=Р\ 63) <2 ВЫВОДИТСЯ по МР ИЗ (2] =
= 0г+0; б4) <3 имеет вид ^ х0/ Д-713 }<п — 1.
Случаи 61) и б2) разбираются точно так же, как при п=1. В 'случае б3) вывод Р-^С) из е имеет такой вид:
1) ВЫВОД Р-^0.г (индуктивное предположение);
2) вывод Р-УС)»-^) (индуктивное предположение);
3) (Р-^(:0^0))-^((Р-^0г)~^(Р-^0)) (тавтология);
4) (Р-^)^(Р-^) (МР к (2) и (3)); •
5) Р-*<2 (МР к (1) и (4)).
В дальнейшем такие рассуждения будут проводиться более кратко, с указанием лишь последних шагов вывода (здесь 3, 4, 5).
Наконец, в случае б4) вывод Р—>? ухС^- из е получается, если добавить к выводу Р-*^у из е (индуктивное предположение) формулы
у х(Р-*(};) ($еп);
ух(Р—<?(},?)—*(Р — ухО.^(зко.тыа в силу замкнутости Р);
Р —? у х(^1 (МР к двум предыдущим формулам).
Лемма доказана.
Отметим для будущего, что во фрагментах выводов, которые строились в леммах 4.4, 4.5, использованы только тавтологии типов А. О., А.1, А.2 из п. 3.4.
Предыдущая << 1 .. 13 14 15 16 17 18 < 19 > 20 21 22 23 24 25 .. 70 >> Следующая

Реклама

c1c0fc952cf0704ad12d6af2ad3bf47e03017fed

Есть, чем поделиться? Отправьте
материал
нам
Авторские права © 2009 BooksShare.
Все права защищены.
Rambler's Top100

c1c0fc952cf0704ad12d6af2ad3bf47e03017fed