о сведении к абсурдному
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 является применением "обычного" принципа док-ва от противного.