о сведении к абсурдному
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}
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)Насколько мне известно, Аппель и Хакен не доказали правильности своей программы с формальной точки зрения. Если бы они это сделали, то это действительно, наверное, являло бы собой пример доказательства того, что существует доказательство, а не самого доказательства; и возможно, в этом одна из причин настороженного отношения многих математиков к их доказательству. Но даже и в их случае нужное формальное доказательство элементано строится конструктивно, просто он слишком длинно для того, чтобы эксплицитно его написать на бумаге, скажем.