aknost: (Default)
[personal profile] aknost
утром сёрфил про Гольфстрим, а вечером увидел репост с похожей основой.
1) передача энергии не требует передачи массы;
2) передача информации не означает передачу значительной энергии;
3) передача информации приводит к изменению массы.
имхо, здесь нет противоречия – всего лишь особенность языка.

Оригинал взят у [livejournal.com profile] sspr в о доказательствах
Оригинал взят у [livejournal.com profile] 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. Исходя из этого факта, Дейкстра протестует против того, чтобы вообще считать принцип бесконечного спуска отдельным принципом, и хвалить того же Ферма за блестящее его применение. Ведь он совершенно эквивалентен индукции, и ничего нового или интересного в нем нет; любое доказательство, использующее его, можно представить в виде доказательства, использующего индукцию.



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



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



July 2017

S M T W T F S
      1
23456 78
9101112131415
16171819202122
23242526272829
3031     

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 22nd, 2017 06:57 pm
Powered by Dreamwidth Studios