о сведении к абсурдному
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 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)