Anatoly Vorobey (avva) wrote,
Anatoly Vorobey
avva

Category:

о сведении к абсурдному

Когда используют метод доказательства от противного (reductio ad absurdum), обычно это получается так:
  • желаем доказать X;
  • предполагаем, что не-X;
  • основываясь на этом предположении, приходим к противоречию;
  • заключаем, что X.
Так этот метод используют со времён древних греков. При этом небезынтересным является тот факт, что противоречие, к которому мы приходим, всегда строится конструктивно на основании нашего "противного" предположения.

Что изменилось с введением формального метода в конце 19-го -- начале 20-го веков? Ничего особенного с точки зрения практического применения метода. Его теоретическое обоснование, однако, получило выражение в качестве мета-математического рассуждения следующего рода, где формальные "строгости" заключены в скобки после неформальных "вольностей":
  • желаем доказать X (желаем получить формальное доказательство утверждения X);
  • предполагаем, что не-X (вводим не-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; но для формального обоснования нужна именно вторая формулировка. Выбор одной из них или разрешение конфликта между ними - это отдельный тонкий вопрос, которого я не хотел касаться в этой записи.
Subscribe
  • Post a new comment

    Error

    default userpic

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 25 comments