о сведении к абсурдному
Jan. 2nd, 2003 07:05 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
avvaКогда используют метод доказательства от противного (reductio ad absurdum), обычно это получается так:
Что изменилось с введением формального метода в конце 19-го -- начале 20-го веков? Ничего особенного с точки зрения практического применения метода. Его теоретическое обоснование, однако, получило выражение в качестве мета-математического рассуждения следующего рода, где формальные "строгости" заключены в скобки после неформальных "вольностей":
В этом заключается разница между методом доказательства от противного и, скажем, правилом модус поненс ("из A и A=>B следует B"), с формальной точки зрения. Модус поненс - правило, позволяющее строить формальные доказательства, переходя в них от одного пункта к другому; доказательство от противного опирается на нашу возможность преобразовывать сами доказательства, обращаясь с ними мета-математически, как с последовательностями символов.
Хорошо.
Но что если возникнет следующая ситуация: из предположения не-X можно будет доказать существование противоречия, но при этом такое доказательство ничего не скажет о том, как именно это противоречие получается из не-X?
Или, говоря более точным языком:
Зафиксируем какую-нибудь формальную систему, в которой мы формализуем математику, скажем, теорию множеств ZFC.
Предположим, я докажу следующее: "если не-X, то ZFC - противоречивая система аксиом, т.е. в ней существует противоречие". То есть, я докажу, что если не-X, то существует некое формальное доказательство, выводящее противоречие из аксиом ZFC; но само это формальное доказательство я не предоставлю, и не будет даже и малейшего намёка на то, как оно может выглядеть. Будет ли это достаточным основанием для того, чтобы считать X доказанным?
С одной стороны, можно утверждать, что будет, следующим образом:
1. Одно из двух: либо ZFC противоречива, либо нет.
2. Если ZFC противоречива, то она доказывает любое утверждение, включая X.
3. Если ZFC непротиворечива, то моё предположение не-X приводит к противоречию, т.к. из него следует, что ZFC противоречива. Значит, моё предположение неверно; следовательно, я могу заключить, что X.
4. В любом случае видим, что ZFC доказывает X.
Здесь третий пункт - не вызывающее никаких проблем использование обычного принципа доказательства от противного в его обычном "эксплицитном" варианте: предполагаем не-X, и приходим к явному противоречию с уже "известными" утверждениями, притом эксплицитным формальным путём. Таким образом, пункты 1-4 вместе представляют собой аргумент, доказывающий "расширенный", "имплицитный" принцип доказательства от противного, с помощью "обычного", "эксплицитного" его варианта.
С другой стороны, мне кажется, возможна вполне практическая проблема: математики могут просто не принять аргумент такого рода в качестве доказательства X. Уж слишком он выглядит неявным, косвенным, не проливающим никакого света на эксплицитное доказательство X из аксиом, не предоставляющий такого доказательства.
Мне не приходит в голову ни один случай действительно случившегося на практике примера применения такого "расширенного" метода доказательства от противного. Если я ничего не упускаю, такого до сих пор просто не было. Но в принципе не видно никаких препятствий к тому, что такое может произойти; и весьма любопытно, каким же будет тогда статус этого доказательства в математическом сообществе.
Наконец, если мы посмотрим на эту гипотетическую возможность с точки зрения обычного формального оправдания метода ad absurdum, объяснённую выше, то увидим следующую картину. Из существования формального доказательства противоречия из ZFC+"не-X" всё ещё следует существование формального док-ва X из ZFC. Но так как первое доказательство не дано эксплицитно (а только доказано его существование), то же самое можно сказать и о втором. Таким образом, в результате мы получаем результат "существует формальное доказательство X из ZFC", не имея при этом никакой информации о том, как именно выглядит это доказательство. Будет ли такой результат принят в качестве удовлетворительного, в качестве доказывающего X?
P.S. Стоит ещё отметить тот факт, что я игнорировал некоторые тонкие различия в вышеописанном аргументе из четырёх пунктов. А именно, различие между "предположив не-X, доказываем существование противоречия из аксиом ZFC" и "доказываем существование противоречия, используя аксиомы ZFC и гипотезу не-X". Первая формулировка более естественна, привычна в качестве основы для применения ad absurdum; но для формального обоснования нужна именно вторая формулировка. Выбор одной из них или разрешение конфликта между ними - это отдельный тонкий вопрос, которого я не хотел касаться в этой записи.
- желаем доказать X;
- предполагаем, что не-X;
- основываясь на этом предположении, приходим к противоречию;
- заключаем, что X.
Что изменилось с введением формального метода в конце 19-го -- начале 20-го веков? Ничего особенного с точки зрения практического применения метода. Его теоретическое обоснование, однако, получило выражение в качестве мета-математического рассуждения следующего рода, где формальные "строгости" заключены в скобки после неформальных "вольностей":
- желаем доказать X (желаем получить формальное доказательство утверждения X);
- предполагаем, что не-X (вводим не-X в качестве формальной гипотезы, что позволяет использовать не-X без дальнейшего обоснования в формальном доказательстве);
- основываясь на этом предположении, приходим к противоречию (находим формальное доказательство формулы вида φ∧¬φ ("φ и не-φ" -- или любой другой фиксированной противоречивой формулы), основываясь на обычных аксиомах плюс формальная гипотеза не-X);
- заключаем, что X (заключаем, что X).
В этом заключается разница между методом доказательства от противного и, скажем, правилом модус поненс ("из A и A=>B следует B"), с формальной точки зрения. Модус поненс - правило, позволяющее строить формальные доказательства, переходя в них от одного пункта к другому; доказательство от противного опирается на нашу возможность преобразовывать сами доказательства, обращаясь с ними мета-математически, как с последовательностями символов.
Хорошо.
Но что если возникнет следующая ситуация: из предположения не-X можно будет доказать существование противоречия, но при этом такое доказательство ничего не скажет о том, как именно это противоречие получается из не-X?
Или, говоря более точным языком:
Зафиксируем какую-нибудь формальную систему, в которой мы формализуем математику, скажем, теорию множеств ZFC.
Предположим, я докажу следующее: "если не-X, то ZFC - противоречивая система аксиом, т.е. в ней существует противоречие". То есть, я докажу, что если не-X, то существует некое формальное доказательство, выводящее противоречие из аксиом ZFC; но само это формальное доказательство я не предоставлю, и не будет даже и малейшего намёка на то, как оно может выглядеть. Будет ли это достаточным основанием для того, чтобы считать X доказанным?
С одной стороны, можно утверждать, что будет, следующим образом:
1. Одно из двух: либо ZFC противоречива, либо нет.
2. Если ZFC противоречива, то она доказывает любое утверждение, включая X.
3. Если ZFC непротиворечива, то моё предположение не-X приводит к противоречию, т.к. из него следует, что ZFC противоречива. Значит, моё предположение неверно; следовательно, я могу заключить, что X.
4. В любом случае видим, что ZFC доказывает X.
Здесь третий пункт - не вызывающее никаких проблем использование обычного принципа доказательства от противного в его обычном "эксплицитном" варианте: предполагаем не-X, и приходим к явному противоречию с уже "известными" утверждениями, притом эксплицитным формальным путём. Таким образом, пункты 1-4 вместе представляют собой аргумент, доказывающий "расширенный", "имплицитный" принцип доказательства от противного, с помощью "обычного", "эксплицитного" его варианта.
С другой стороны, мне кажется, возможна вполне практическая проблема: математики могут просто не принять аргумент такого рода в качестве доказательства X. Уж слишком он выглядит неявным, косвенным, не проливающим никакого света на эксплицитное доказательство X из аксиом, не предоставляющий такого доказательства.
Мне не приходит в голову ни один случай действительно случившегося на практике примера применения такого "расширенного" метода доказательства от противного. Если я ничего не упускаю, такого до сих пор просто не было. Но в принципе не видно никаких препятствий к тому, что такое может произойти; и весьма любопытно, каким же будет тогда статус этого доказательства в математическом сообществе.
Наконец, если мы посмотрим на эту гипотетическую возможность с точки зрения обычного формального оправдания метода ad absurdum, объяснённую выше, то увидим следующую картину. Из существования формального доказательства противоречия из ZFC+"не-X" всё ещё следует существование формального док-ва X из ZFC. Но так как первое доказательство не дано эксплицитно (а только доказано его существование), то же самое можно сказать и о втором. Таким образом, в результате мы получаем результат "существует формальное доказательство X из ZFC", не имея при этом никакой информации о том, как именно выглядит это доказательство. Будет ли такой результат принят в качестве удовлетворительного, в качестве доказывающего X?
P.S. Стоит ещё отметить тот факт, что я игнорировал некоторые тонкие различия в вышеописанном аргументе из четырёх пунктов. А именно, различие между "предположив не-X, доказываем существование противоречия из аксиом ZFC" и "доказываем существование противоречия, используя аксиомы ZFC и гипотезу не-X". Первая формулировка более естественна, привычна в качестве основы для применения ad absurdum; но для формального обоснования нужна именно вторая формулировка. Выбор одной из них или разрешение конфликта между ними - это отдельный тонкий вопрос, которого я не хотел касаться в этой записи.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2003-01-02 10:33 am (UTC)По поводу "P.S.". Мне кажется, что #1 есть лишь разговорная форма #2, если не вкладывать в #1 намеренно нерезонный смысл. Или есть "резонная" разница.
no subject
Date: 2003-01-02 10:34 am (UTC)Re:
Date: 2003-01-02 04:19 pm (UTC)А откуда такая уверенность, что будет? У меня её нет.
По поводу "P.S.". Мне кажется, что #1 есть лишь разговорная форма #2, если не вкладывать в #1 намеренно нерезонный смысл. Или есть "резонная" разница.
Вопрос, однако, в том, действительно ли #2 является применением "обычного" принципа док-ва от противного.
no subject
Date: 2003-01-02 11:00 am (UTC)Если такие есть, то переделать их под доказательство от противного должно быть делом техники.
Я только знаю похожий пример, Теорему Геделя и иже с ней, но там доказывается *несуществование* доказательства.
Re:
Date: 2003-01-02 02:29 pm (UTC)Мне, по крайней мере, неизвестны такие случаи.
Но я не вижу причин, по которым они не могут существовать.
Я только знаю похожий пример, Теорему Геделя и иже с ней, но там доказывается *несуществование* доказательства.
Да, это совсем другой случай. Хотя я как раз вспоминал аргумент док-ва второй теоремы о неполноте, когда мне эта мысль (этой записи) пришла в голову.
no subject
Date: 2003-01-03 03:44 pm (UTC)Многие математики этот результат не приняли именно по причине его косвенности. (Хотя, кажется, не так давно появилось альтернативное док-во: http://www.math.gatech.edu/~thomas/FC/fourcolor.html )
Другой, более надуманный пример (из теории компиляторов):
Возьмем какую-нибудь более-менее навернутую LR(1) грамматику G и рассмотрим вопрос: удовлетворяет ли строчка S правилам этой грамматики. Ответить на этот вопрос легко - берешь синтаксический анализатор, соответствующий G, и пропускаешь строчку через него. Фишка в том, что в большинстве случаев такой анализатор может быть построен только программно. Для человека это чересчур сложно.
То есть, мы доказываем правильность генератора анализаторов, из чего мы делаем вывод, что ответ, выданный сгенерированным анализатором тоже является верным. Пусть интуицмонисты скрежещут зубами, сколько им угодно, а многие современные компиляторы именно так и написаны.
(Там дело еще навернутее - ибо сам генератор компиляторов написан на Си и соответственно его правильность зависит от правильности компилятора Си, который сам, скорее всего, был автоматически сгенерирован)
Re:
Date: 2003-01-12 09:28 am (UTC)Насколько мне известно, Аппель и Хакен не доказали правильности своей программы с формальной точки зрения. Если бы они это сделали, то это действительно, наверное, являло бы собой пример доказательства того, что существует доказательство, а не самого доказательства; и возможно, в этом одна из причин настороженного отношения многих математиков к их доказательству. Но даже и в их случае нужное формальное доказательство элементано строится конструктивно, просто он слишком длинно для того, чтобы эксплицитно его написать на бумаге, скажем.
no subject
Date: 2003-01-02 04:02 pm (UTC)>>Из существования формального доказательства противоречия из ZFC+"не-X" всё ещё следует существование формального док-ва X из ZFC. Но так как первое доказательство не дано эксплицитно (а только доказано его существование), то же самое можно сказать и о втором.
Рассмотрим утверждения A - "существует формальное доказательство противоречия из ZFC+"не-X", и B - "существует формальное доказательство X из ZFC". Тогда утверждения "не-A" и "не-B" будут соответственно "не существует формального доказательства противоречия из ZFC+"не-X" и "не существует формального доказательства X из ZFC". У Вас из того, что A влечет B, следует, что "не-A" влечет "не-B". Понятно, что это логическая ошибка. Впрочем, она несущественна, поскольку вопросы, поставленные Вами, все равно будут актуальны - правда, только в теоретическом плане (получить результат "существует формальное доказательство X из ZFC" можно, но не потому, что верно "не-A"), а в практическом плане (доверие ученых к такому доказательству) всё сводится к тому, интуиционист вы, логицист или формалист. Интуиционисты, например, вообще не признавали "не-формальных" доказательств, как и многого другого. Логицистам же ничто не мешает признать за доказательство "существование существования несуществования существования" или чего угодно в этом плане.
Любопытно, что рассматривая принцип доказательства "от противного", Вы допустили ошибку в этом самом принципе. В нашем случае неравноправие утверждений A и B возникло как раз из того, что для принципа "от противного" не существует обратного, т.е. из B не следует A.
Re:
Date: 2003-01-02 04:08 pm (UTC)Я думаю, что Вы меня неправильно поняли. Я вовсе не утверждаю, что из не-А следует не-Б. Я утверждаю вот что: из А следует Б, но если А не дано эксплицитно (а только доказано его существование), то и Б не будет дано эксплицитно (а только будет доказано его существование).
Я нигде не утверждаю "не-А". Я рассматриваю ситуацию, при которой будет доказано А - существование формального док-ва противоречия -- но при этом не будет предъявлено явное формальное доказательство, будет только доказано его существование. Это не "не-А", это определённый вид А, который на практике вроде бы пока не встречался, но мне интересно, что случится, если он встретится.
Re:
Date: 2003-01-02 04:18 pm (UTC)Прошу прощения.
no subject
Date: 2003-01-02 04:22 pm (UTC)Re:
Date: 2003-01-02 04:28 pm (UTC)Я писал о похожей проблеме в теории вычислимости несколько раз уже, например:
http://www.livejournal.com/talkread.bml?journal=avva&itemid=507455
http://www.livejournal.com/talkread.bml?journal=avva&itemid=353811
Сегодняшняя запись про док-ва от противного - просто быстрый отчёт о том, что пришло в голову сегодня в кафе, чтобы не потерялось :)
no subject
Date: 2003-01-02 04:16 pm (UTC)Я думаю, что Вы меня неправильно поняли. Я вовсе не утверждаю, что из не-А следует не-Б. Я утверждаю вот что: из А следует Б, но если А не дано эксплицитно (а только доказано его существование), то и Б не будет дано эксплицитно (а только будет доказано его существование).
Если быть совсем точным, то даже так:
Я вовсе не утверждаю, что из не-А следует не-Б. Я утверждаю вот что: из А следует Б. Но если А доказывается неконструктивно, т.е. доказательство А не даёт информации о том, как выглядит формальное док-во, существование которого доказывает А, то то же самое будет верно касательно формального док-во, существование которого докажет Б.
Обозначим через P1 формальное доказательство противоречия из не-X+ZFC , и через P2 - формально е доказательство X из ZFC. Тогда:
А = "существует P1"
B = "существует P2"
A=>B верно как метаматематическая теорема (для её формализации и доказательства, более того, в принципе достаточно довольно слабой системы аксиом, но это уже другая тема).
Но если доказательство A неконструктивно -- не предъявляет эксплицитно P1, то и док-во B тоже не предъявит эксплицитно P2.
В обычной математической практике неконструктивные доказательства утверждений типа A пока что не встречались, если я ничего не упустил. Но я не вижу принципиальных препятствий к тому, чтобы они были возможны.
Re:
Date: 2003-01-02 04:24 pm (UTC)Вот это почему, я не понял.
Re:
Date: 2003-01-02 04:39 pm (UTC)Есть процедура, позволяющяя перевести P1 в P2. Есть доказанное утверждение о существовании P1. Из этого можно получить доказанное утверждение о существовании P2. Но само P2 в явном виде можно получить, только если P1 дано в явном виде.
Re:
Date: 2003-01-02 04:53 pm (UTC)Re:
Date: 2003-01-02 04:56 pm (UTC)Вопрос в приемлемости доказательства существования P2, полученного именно таким образом (без самого P2 в явном виде).
no subject
Date: 2003-01-03 02:45 am (UTC)no subject
Date: 2003-01-03 07:42 am (UTC)no subject
Date: 2003-01-04 04:13 am (UTC)Re:
Date: 2003-01-04 09:07 am (UTC)no subject
Date: 2003-01-04 09:20 am (UTC)no subject
Date: 2003-01-04 09:27 am (UTC)Из предположения не-X в Вашем примере строится доказательство противоречия в ZFC конструктивным (даже тривиально вычислимым) образом. Именно потому, что модели Гёделя на самом деле синтаксические, а не семантические. В точности так, как я хочу было бы, если бы из not(Con(ZFC+GCH)) доказывалось существование противоречия в ZFC без эксплицитного построения такого противоречия; например, доказывалось бы, что у ZFC нет модели (семантической модели, модели-множества).
Так мне кажется, хотя сейчас вообще-то голова не очень работает.
no subject
Date: 2003-01-04 09:55 am (UTC)Re:
Date: 2003-01-12 09:25 am (UTC)