о доказательствах

[avva]

В одной из своих замечательных заметок (англ., PDF) Дейкстра протестует против, по его мнению, вредного и приводящего к путанице понятия косвенного доказательства. Если, желая доказать A--->B (из A следует B), мы начинаем с предположения "не-B", и доказываем исходя из этого "не-A", это называется косвенным доказательством (в отличие от прямого доказательства, когда мы предполагаем A и доказываем B напрямую).

Дейкстра считает, что разделять эти два метода - нелепо, и они есть одно и то же. Действительно, с точки зрения чистой логики утверждения A--->B и (не-B)--->(не-A) совершенно эквивалентны, и доказать одно означает доказать другое. Собственно, они оба тождественно утверждению "не-A или B", которое Дейкстра предлагает считать более фундаментальным, чем обе эти версии.

Дейкстра неправ. Математики не просто так и не из соображений устаревшей терминологии называют некоторые доказательства прямыми, а другие - косвенными. Несмотря на формальную тождественность, между ними есть существенная разница с точки зрения математической практики. Но как это продемонстрировать?

Обратимся к еще одному примеру вредной терминологии с точки зрения Дейкстры, тесно связанному с только что упомянутым. Принцип математической индукции можно сформулировать следующим образом: если мы хотим доказать какой-то предикат (какое-то свойство) P(x) для любого натурального числа x (x = 0, 1, 2, ...), то нам достаточно доказать следующее: из того, что P выполняется для всех y меньше x, следует, что P выполняется для x. В символьном виде (∀x читается "для каждого икс...", а ∃x - "существует икс такой, что...", и эти два символа называются кванторами общности и существования): (∀y)(y<x ---> P(y)) ---> P(x). Еще раз словами: если для любого y верно, что из того, что y меньше x следует истинность P(y), тогда верно и P(x). Если мы докажем это, то принцип математической индукции гласит, что мы доказали P(x) для любого x.

(более привычная формулировка индукции, когда переходят от P(n) к P(n+1), является частным и несколько более слабым вариантом. В более общей формулировке, приведенной выше, для доказательства P(n+1) нам разрешено пользоваться не только доказанностью для предыдущего числа, P(n), но и для всех чисел, уже доказанных до сих пор, начиная с 0 - переменная y как раз и пробегает весь их список).

С другой стороны, принцип бесконечного спуска - приоритет сознательного и плодотворного его использования принадлежит Ферма - является вариантом принципа математической индукции, хоть это может и не быть очевидным заранее. При использовании принципа бесконечного спуска, желая доказать P(x) для всех x, мы доказываем следующее: если для какого-то x верно ¬P(x) (¬ означает отрицание: "не-P(x)"), то существует какое-то y меньше x, для которого тоже верно ¬P(y). Если мы докажем это, то принцип бесконечного спуска гласит, что мы доказали P(x) для всех x. С интуитивной точки зрения это объясняется так: если P(x) неверно хотя бы для какого-то x, то доказанное нами утверждение позволяет построить нисходящую цепочку таких иксов, для которых P неверно: начиная с x, потом какой-то x' меньше его, потом x'' меньше этого, и так далее без конца. Но не бывает бесконечной нисходящей цепочки натуральных чисел (не бывает "бесконечного спуска"): если, например, мы начали цепочку с числа 1000, то дальше в ней может быть не больше тысячи членов, но никак не бесконечное число.

Это может показаться неочевидным, но принцип бесконечного спуска совершенно тождественен принципу математической индукции: это один и тот же принцип. При использовании индукции мы стремились доказать следующее (в символьном виде):

(∀y)(y<x → P(y)) → P(x)

Если мы теперь "перевернем" это утверждение (т.е. от A→B перейдем к эквивалентному ¬B→¬A), то получим

¬P(x) → ¬(∀y)(y<x → P(y))

Используя формулы, связывающие два квантора, а именно тот факт, что ¬∀ эквивалентно ∃¬ (словами: если неверно, что "для всех x" выполняется то-то и то-то, то "существует" какой-то x, для которого не выполняется то-то и то-то), это можно записать как

¬P(x) → (∃y)¬(y<x → P(y))

А отрицать утверждение (y<x → P(y)) - все равно, что сказать, что его условие выполняется, а следствие - нет, т.е. одновременно верно y<x и ¬P(y), и сделав эту замену, мы приходим (используя символ ∧ в значении "и") к

¬P(x) → (∃y)(y<x ∧ ¬P(y))

что является в точности тем, что нам полагается доказать для применения принципа бесконечного спуска: если неверно P(x), то есть какой-то y, который меньше x, и для которого неверно P(y).

Таким образом, с точки зрения чистой логики два этих принципа совершенно тождественны, подобно тому, как тождественны "прямое" доказательство A → B и "косвенное" ¬B → ¬A. Исходя из этого факта, Дейкстра протестует против того, чтобы вообще считать принцип бесконечного спуска отдельным принципом, и хвалить того же Ферма за блестящее его применение. Ведь он совершенно эквивалентен индукции, и ничего нового или интересного в нем нет; любое доказательство, использующее его, можно представить в виде доказательства, использующего индукцию.

Дейкстра неправ. Математики не просто так используют разные названия, когда говорят об этих двух принципах. Хотя с точки зрения формальной логики они и тождественны, есть доказательства, "естественным" образом использующие индукцию, а есть доказательства, "естественным" образом использующие принцип бесконечного спуска. Но что это значит - "естественным образом", и как это продемонстрировать?

Об этом - через час-два в следующей записи :)

Comments

[cryinstone.livejournal.com]

Не совсем:
с точки зрения чистой логики, утверждения A--->B и (не-B)-->(не-А) совершенно эквивалентны.

[avva.livejournal.com]

Да, конечно. Просто опечатка, сейчас исправлю, спасибо.

[aburachil.livejournal.com]

Косвенным доказательством это не называют. Бэрусит омрим "доказательство от противного" :-)

[avva.livejournal.com]

Нет. Док-во от противного, это, желая доказать A, начинаем с ¬A и приходим к противоречию. Я сам не уверен в точности в том, как называют по-русски indirect proof, но словари сказали "косвенное" и я решил на них положиться.

[pussbigeyes.livejournal.com]

Вы неправы. Доказательство от противного - это именно то, что Вы называете непрямым, или косвенным, доказательством.

Любое математическое утверждение формулируется в виде "если А, то В". Даже утверждения типа "для всех x выполнено Р(х)", поскольку мы заранее обладаем некоторой информацией о множестве всех х и свойстве Р. Можно переформулировать его в виде "если х - любое, то Р(х)". Доказательство от противного: предположим, что "не В", тогда "не А". Противоречие, поскольку мы предполагали, что А.

[crazy-flyer.livejournal.com]

ИМХО , это всё же разные вещи . Если мы хотим доказать В , то вовсе не обязательно придумывать предварительное условие А , чтобы потом доказывать А ---> В . Да и какое условие можно придумать для доказательства утверждения , например , что "любое квадратное уравнение имеет два комплексных корня" , или , "существует хотя бы одно действительное число" ? Опять-таки , если мы доказываем от противного утверждение В , то нам надо предположить не-В , и прийти к ЛЮБОМУ противоречию . То есть к противоречию с ЛЮБЫМ истинным утверждением , а не только с каким-то А . Мы , начиная доказательство от противного , можем заранее и не знать , к какому противоречию придём . А потребовав условие А , мы должны обязательно прийти к не-А , что может значительно затруднить доказательство .

[pussbigeyes.livejournal.com]

Доказательство от противного - весьма общий подход. То, что Вы описываете, - частный случай общего. "Любое истинное утверждение" формально играет роль предположения А. На Ваших примерах: определения понятий "комплексное число", "квадратное уравнение", "корень уравнения" с соответствующей аксиоматикой составляют содержательную часть предположения; та же история с понятием "действительное число". Переформулируйте в виде "если назвать действительным числом то-то и то-то (А), то действительные числа существуют (В)".

Другими словами, любое содержательное утверждение предполагает наличие хотя бы одного не исчерпывающегося им самим утверждения, которое считается истинным. В таковой роли могут выступать и аксиомы. Именно это утверждение естественным образом выступает в качестве предположения А. Прийти к противоречию, предположив "не-В" и не обладая никакой доказательной базой, невозможно.

[(Anonymous)]

математик, ё

лучше бы уж молчал

[nine_k]

"Дейкстра неправ" -- это даже круче, чем "goto considered harmful" ;)

Вообще вся математика эквивалентна набору аксиом ZFC. Все эти тождества, которые так старательно развивтают математики вместо того, чтобы аксиомами и ограничиться, есть мыслительные подпорки, этакий кэш логических выкладок. И различие между "методом индукции" и "методом бесконечного спуска" именно в характере обеспеиваемой ими ментальной подпорки, а не в сущности. Т.е. Дейкстра прав -- но не в том :)

[kapahel.livejournal.com]

::Вообще вся математика эквивалентна набору аксиом ZFC.
Ну уж.

[faceted-jacinth.livejournal.com]

По духу 9000 прав, так и есть, если не рассматривать непонятные вещи вроде "парадигм".

А вопросом о том, эквивалентна ли математика ZFC (кстати, почему С? Она ж весьма спорная) занимаются философы с математическим образованием, сиречь математики, задолбавшиеся доказывать разные утверждения и пытающиеся понять, зачем и нужно ли их вообще доказывать.

[kapahel.livejournal.com]

1) Вся математика определенно не эквивалентна ZFC (например, есть разные топосы).
2) Повседневная рабочая практика большинства математиков никак не связана с ZFC, а связана с изучением некоторой, прошу прощения, объективной реальности. Многое можно -- но только в принципе -- свести к ZFC (потому что принято доказывать утверждения), но при чем тут математика? Мысль, прямо скажем, банальная, но все же.

[archernikov.livejournal.com]

Ох, да это вообще дико слышать каждый раз. ZFC - такой же объект для математического изучения, как и любой другой.

[kapahel.livejournal.com]

Что "это"?

[archernikov.livejournal.com]

Высказывания в духе 9000(я уже вроде видел ваш обмен репликами подобного содержания) и faceted_jacinth. Наверное это какие-то порочные эффекты популяризации. Т.е. представить себе модель ZFC всё-таки несколько сложнее, чем группу или многообразие, но обращаются то на практике с ними точно так же.

[kala-hansa.livejournal.com]

Блин, о чем люди по ночам думают..)))*недоумевая, но таки восхищаясь

[french-man.livejournal.com]

Я стараюсь избегать доказательств от противного где только возможно.

[aburachil.livejournal.com]

Мне такая позиция знакома, а почему собственно? Иногда бывает возможно, но проще понять от противного.

[french-man.livejournal.com]

Во многих случах рассуждения ad absurdum затмевают суть дела. Изложишь прямо - и все становится яснее и элегантнее. Мне кажется, от абсурда лучше решать задачу (предположим, что оно не так, и что?) Но, решив, лучше излагать прямо.

[faceted-jacinth.livejournal.com]

Не так.
В реальной жизни иногда случаются вопросы, на которые нельзя ответить "да" или "нет". В математике, кстати, тоже. Поэтому доказательство от противного имеет доказательную силу пока сохраняется уверенность в том, что кроме ответа "нет" есть единственная альтернатива.

Кстати интересно, как Вы собираетесь доказывать не от противного неравенство мощностей натуральных и вещественных чисел?

[french-man.livejournal.com]

Я абсолютно ничего не говорил о доказательной силе. Разумеется, я стопроцентно признаю доказательную силу рассуждений от противного, и сам их применяю. Я лишь полагаю, что в печатных текстах их лучше избегать. Не потому, что они «менее доказательны», а потому, что они менее элегантны.

[faceted-jacinth.livejournal.com]

Хм.
А всё же.
Известно ли Вам более элегантное доказательство неравномощности вещественных и натуральных чисел, чем от противного?

Если Ваш ответ заведомом не принесёт мне ничего нового, лучше его и не пишите, я ж не для спора сюда встрял, а ради Знания, как ни пафосно это не прозвучит.

[french-man.livejournal.com]

Я не утверждаю, что доказательства от противного ВСЕГДА менее элегантны. Я утверждаю, что они чаще всего менее элегантны, чем соответсвующие прямые д-ва. Но, разумеется, есть немало исключений.

[avva.livejournal.com]

Пусть f:N->R. Построим вещественное число r, у которого целая часть 0, а десятичное разложение после запятой определяется по индукции так, что его n-я цифра не равна n-ой цифре числa f(n). Для каждого n верно, что f(n) ≠ r. Следовательно, r не принадлежит f(N). Следовательно, f(N) ≠ R. Следовательно, f не является биекцией между N и R. Поскольку мы не накладывали на f никаких условий, из этого следует, что не существует биекции между N и R.

Не от противного, верно?

Как раз в данном случае, мне кажется, нет существенной разницы между прямым доказательством и от противного.

[faceted-jacinth.livejournal.com]

Да, не от противного.

Не знаю, просто лично мне доказательство от противного кажется эдакой жемчужиной, найденной математиками в море разнообразных методов доказательства. Оно простое, красивое, мощное и удобное - если привыкнуть немножко.

Ой, "на вкус и цвет все фломастеры разные", и тут это применимо в полной мере. Это спор о вкусах.

[avva.livejournal.com]

Действительно еще проще, спасибо.

[ppetya.livejournal.com]

Лучше уж (так не используется десятичное разложение) строить сразу стягивающуюся в точку систему вложенных отрезков, так что n-й отрезок не содержит первых n членов последовательности. Он и стянется к точке вне f(N).

[french-man.livejournal.com]

Вот именно это я имею в виду, говоря, что прямые д-ва изящнее и элегантнее.

[ppetya.livejournal.com]

А Вы какое доказательство имеете в виду?

[ppetya.livejournal.com]

Признаю доказательную силу рассуждений от противного на 60%!

Давно понял, что ничего стоящего не придумаешь, если изначально думать "от противного". "Противного" и бессмысленного слишком много.

[french-man.livejournal.com]

Ты противный. Я по тебе скучаю.

[ppetya.livejournal.com]

Надеюсь провести весну в Нанте. Не от меня пока зависит. Я бы к вам тогда заехал.

Кому что противно, рассказали недавно --

"Меня милый не целует,
Не пускает близко.
Я, мол, чистый математик,
а ты программистка."

[(Anonymous)]

лучше бы промолчал, ей-богу

прочитайте еще раз сообщение, на которое отвечаете и перестаньте тупить

[french-man.livejournal.com]

Какой-то аноним нервный пошел. Выпейте коньяку и расслабьтесь.

[maxint.livejournal.com]

> Еще раз словами: если для любого y верно, что из того, что y меньше x следует
> истинность P(y), тогда верно и P(x). Если мы докажем это, то принцип
> математической индукции гласит, что мы доказали P(x) для любого x.

I believe at Fiz-Tech they called this "The Method of Partial (or Female) Induction".
What about the "initial step" - so called basis? (See http://en.wikipedia.org/wiki/Mathematical_induction (http://en.wikipedia.org/wiki/Mathematical_induction))

[avva.livejournal.com]

The initial step is included because when x is 0, the condition "for all y < x, P(y)" is satisfied vacuously, and therefore what we have to prove in this case is precisely P(0).

[maxint.livejournal.com]

yep, especially if you take zero to be a natural number...

[avva.livejournal.com]

Which you usually do when discussing proof theory, metamathematics, induction principles, etc.

Может быть, но нет!...

[mellonis.livejournal.com]

A--->B и (не-B)--->(не-A) - это не тождественные утверждения. Их не-В может следовать не-А, но это не говорит, что из А не следует В.

Re: Может быть, но нет!...

[crazy-flyer.livejournal.com]

Вот это как раз неверно ! Не тождественны выражения A--->B и (не-A)--->(не-B) , это точно .

Re: Может быть, но нет!...

[mellonis.livejournal.com]

Ой, а я не умею, как ты, читать между строк.... :-P

[grur.livejournal.com]

Мне кажется, в интуиционистской логике прямое и обратное доказательства могут быть неэквивалентны, поскольку не выполняется принцип исключенного третьего...

[(Anonymous)]

конечно

просто не на все вопросы есть однозначный ответ "да" или "нет". (иными словами, есть принципиально неразрешимые задачи.)

это вполне доказанный закон природы.

[habaroff.livejournal.com]

осилил до половины и завис... сцука разрушитель мозга я не готов к таким экспериментам