Корень всех проблем

[kostiani]

Профессор Снэйп в сообщении #621021 писал(а):

Да ну откуда круг-то? Вы что, намекаете, что при коммунизме царь комунны будет считаться рабом самого последнего раба?!

Он будет царем самого последнего царя!

[Munin]

epros в сообщении #620915 писал(а):

А вот фишка в том и есть, что ничего добавить нельзя.

С тем, что вы не можете внятно объяснить каких-то простых вещей, я уже сталкивался. Подожду, что Профессор Снэйп на мой вопрос ответит.

[Профессор Снэйп]

Munin в сообщении #621031 писал(а):

Подожду, что Профессор Снэйп на мой вопрос ответит.

Я тут с ходу даже не знаю, за какой хвостик ухватиться, чтоб верёвочку распутать

Наверное начну со следующего: "доказуемость" или "выводимость" (это действительно синонимы) означает, что утверждение можно получить в рамках формальной логики, в соответствии с заранее заданными аксиомами и правилами вывода. А истинность - это то, что имеется "де факто". Самый такой грубый пример... допустим, у мальчика строгая мама и она не отпускает его гулять, пока он не сделает уроки. Но в один прекрасный день мама делала ремонт в квартире, надышалась краски и отпустила мальчика гулять, не проверив домашнее задание. Получается, что утверждение "мальчик не сделал уроки и пошёл гулять на улицу" истинно, но не доказуемо. Не доказуемо, потому что если знать всё про маму и ничего не знать про краску, то логически это вывести ну никак не можно... А истинно... вот он мальчик на улице, с ребятами футбол гоняет, а вот его пустая тетрадь, все желающие могут посмотреть и убедиться!!!

Естественно, что логические правила, позволяющие что-то доказывать, вводят, исходя из двух критериев:

1) Всё доказуемое должно быть истинно! Иначе нахрена нам такая логика?!
2) Желательно, чтоб как можно больше истинных вещей были доказуемыми.

Второе, увы, недостижимый идеал (теоремы о неполноте и всё такое...), но, поелику это возможно, к нему стремятся.

Это, так сказать, прелюдия. А теперь основное. Понимание того, что значит "истинно", может быть разным. В классической и конструктивной математиках разница проявляется прежде всего в экзистенциальных суждениях (то есть утверждениях с квантором существования). Для классического математика истинность утверждения $\exists x \Phi(x)$ означает, что некий абстрактный $x$ со свойством $\Phi$ существует, несмотря на то, что может не быть никакого эффективного способа нахождения такого икса. Классический математик считает утверждение $\exists x \Phi(x)$ истинным, если он предположил $\forall x \neg \Phi(x)$ и пришёл к противоречию. Для него $x$ либо существует, либо не существует, и если он пришёл к выводу, что несуществование невозможно, то тем самым он считает существование доказанным. Несмотря на то, что он не привёл никакого конкретного икса со свойством $\Phi$ и не показал, как его можно найти. Конструктивист же понимает утверждение о существовании икса как утверждение о наличии некоего конкретного способа его нахождения! И если конструктивист опроверг утверждение $\forall x \neg \Phi(x)$, то он не считает, что тем самым доказал $\exists x \Phi(x)$, поскольку опровержение могло быть весьма и весьма косвенным... В частности, таким, которое не указывает, как находить конкретный $x$ со свойством $\Phi$. В этом смысле закон исключённого третьего для классического математика истинен, а для конструктивиста ложен. Классический математик верит в то, что существование не зависит от возможности нахождения конкретного, и поэтому он просто кладёт закон исключённого третьего в свою логику. Для конструктивиста существование суть возможность нахождения, поэтому он не считает существование доказанным до тех пор, пока не указан конкретный способ нахождения. Опровержение утверждения о том, что икс не существует, может не давать способа нахождения икса, поэтому и самого существования оно не доказывает

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

Я, кстати, не поклонник конструктивной математики. А вот epros вроде бы убеждённый конструктивист Разница между нами - она, прежде всего, идеологического плана.

Это была попытка следующего приближения... опять же достаточно грубая, но чуть более точная, чем предыдущая. Если углубляться далее, то надо копать в различие между конструктивизмом и интуиционизмом. То, что я сейчас говорил про различие между классиками и конструктивистами, применимо также к разнице между классиками и интуиционистами. И интуиционисты, и конструктивисты не признают закон исключённого третьего; и те, и другие понимают существование как возможность в некотором смысле "явного" построения объектов с заданными свойствами. Однако между конструктивистами и интуиционистами есть отличие. Но оно уже более тонкое

-- Ср сен 19, 2012 21:14:44 --

Кстати, самые последовательные конструктивисты даже истинность дизьюнкции $\Phi \vee \Psi$ понимают как возможность указать конкретный истинный член дизьюнкции. То есть сказать конкретно, $\Phi$ истинно или $\Psi$. И для них может не быть истинным утверждение $\Phi(x) \vee \neg\Phi(x)$, если они не имеют алгоритма, который бы для каждого конкретного $x$ указывал, истинно $\Phi$ для него или ложно.

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

Представляете, как люди осложняют себе жизнь!

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

[Munin]

Профессор Снэйп в сообщении #621068 писал(а):

И если конструктивист опроверг утверждение $\forall x \neg \Phi(x)$, то он не считает, что тем самым доказал $\exists x \Phi(x)$, поскольку опровержение могло быть весьма и весьма косвенным...

Хорошо, а что он в таком случае доказал? Или опроверг и доказал тоже оказываются не обратными друг к другу?

Какие получаются законы алгебры логики, и законы работы с кванторами? Можно ли обойтись в минимальном варианте алгебры логики по-прежнему двумя значениями $\{0,1\},$ или приходится вводить какие-то ещё?

Профессор Снэйп в сообщении #621068 писал(а):

Я, кстати, не поклонник конструктивной математики. А вот epros вроде бы убеждённый конструктивист :lol: Разница между нами - она, прежде всего, идеологического плана.

Это наиболее феерическая для меня часть истории. Как если бы один математик был убеждённым евклидовцем, а другой - убеждённым лобачевцем. Очевидно же, что при работоспособности двух систем можно свободно пользоваться обеими, оговаривая изначально, о чём речь.

Профессор Снэйп в сообщении #621068 писал(а):

У классиков тоже есть подобные фишки. Например, утверждение: "существует мощность, промежуточная между счётной бесконечностью и континуумом" тоже в каком-то смысле не истинное и не ложное, а какое-то "неопределённое", как точные координаты электрона в пространстве вкупе с его точным импульсом

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

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

[Профессор Снэйп]

Munin в сообщении #621102 писал(а):

Хорошо, а что он в таком случае доказал?

Он доказал $\neg\forall x \neg\Phi(x)$. Ну, или $\neg\neg\exists x \Phi(x)$. Для конструктивиста $\neg\neg\varphi$ не равносильно $\varphi$

-- Ср сен 19, 2012 22:09:12 --

Munin в сообщении #621102 писал(а):

Какие получаются законы алгебры логики, и законы работы с кванторами?

Для начала такие

Кванторов тут пока ещё нет, но фундамент уже заложен. Он беднее, чем в классической логике: в частности, $\neg\neg\Phi \rightarrow \Phi$ не выводимо. Далее уже на это кванторы наворачивают...

[gris]

Про рабов. Сказано: самый последний землепашец. Значит от первого до предпоследнего никаких рабов иметь не будут. И эти два раба не будут землепашцами вообще. Прямо брадобрей, понимаешь!
Вы мелкий шрифт в договоре читали? Да мало ли, как вы его понимали!

[Профессор Снэйп]

Munin в сообщении #621102 писал(а):

Насколько я знаю, оно не "неопределённое", а независимое от аксиоматики ZFC, то есть его можно произвольно добавлять и отрицать, как Пятый постулат в геометрии.

Ну а как насчёт его "истинности"? Доказуемо в ZFC или не доказуемо - несколько другой вопрос... Тут не в том фишка, что можно или что не можно добавить, а в том, что следует добавить

[Munin]

Профессор Снэйп в сообщении #621068 писал(а):

какое-то "неопределённое", как точные координаты электрона в пространстве вкупе с его точным импульсом

Скажу вам всё-таки своё фи. Про эту неопределённость ходит много мифов, и к сожалению, даже среди серьёзных людей, скажем, математиков, биологов, но не физиков, легко встретить такие мифы в голове, вместо стандартного "не знаю, это далеко не моя область".

Существуют состояния $s\in S,$ в которых может находиться электрон. Существуют функции, которые дают координату электрона, $x(s)\in X,$ и импульс электрона, $p(s)\in P.$ Во времена классической физики были исследованы только некоторые состояния $S_c\subset S,$ и для них было известно, что у электрона есть такая штука, как координата, и такая штука, как импульс, и их всегда можно измерить, $S_c\subseteq D(x(s)),$ $S_c\subseteq D(p(s)).$ Но потом была открыта квантовая физика - были открыты новые состояния $S\setminus S_c,$ и для них оказалось, что старые функции просто не продолжаются на новую область, $S\nsubseteq D(x(s)),$ $S\nsubseteq D(p(s)).$ Назойливым философам объяснили, что "мы не можем их определить, это неопределённость", но для себя физики хорошо поняли, что этих функций просто не существует. (Есть другие, и их успешно используют, чтобы подробно описывать все $s\in S,$ и эволюцию во времени $s(t),$ и другие физические свойства и законы.)

[Профессор Снэйп]

Munin в сообщении #621102 писал(а):

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

Не, ну чисто из соображений экономии мышления, если удобно.

Это как отношение евклидовой и неевклидовой геометрий к физике. И та, и другая модель внутренне непротиворечивы и погружаются одна в другую, но вопрос о том, в какой модели мы реально живём, лежит в несколько иной плоскости.

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

[Munin]

Профессор Снэйп в сообщении #621104 писал(а):

Для начала такие

Так, кроме закона исключённого третьего, отличие от Гильберта во второй аксиоме:
$(\text{constr})\qquad ((A\to B)\to ((B\to C)\to (A\to C)))$
$(\text{classic})\qquad ((A\to (B\to C))\to ((A\to B)\to (A\to C)))$
Это что-то значит, или равносильно?

И хотелось бы какую-нибудь наглядную модельку, типа булевой алгебры для обычной логики.

gris в сообщении #621106 писал(а):

Про рабов. Сказано: самый последний землепашец. Значит от первого до предпоследнего никаких рабов иметь не будут. И эти два раба не будут землепашцами вообще.

Или они могут просто раньше в очереди стоять...

Профессор Снэйп в сообщении #621108 писал(а):

Ну а как насчёт его "истинности"? Доказуемо в ZFC или не доказуемо - несколько другой вопрос... Тут не в том фишка, что можно или что не можно добавить, а в том, что следует добавить

А никак насчёт его "истинности". Не существует такой вещи, как "истинность". В геометрии Евклида Пятый постулат истинен, в геометрии Лобачевского - ложен. "Следует добавить" тоже неправильно: следует добавить, если мы хотим получить геометрию Евклида, а если мы хотим чего-то другого, то напротив, не следует добавлять.

[Профессор Снэйп]

Munin в сообщении #621111 писал(а):

Скажу вам всё-таки своё фи. Про эту неопределённость ходит много мифов, и к сожалению, даже среди серьёзных людей, скажем, математиков, биологов, но не физиков, легко встретить такие мифы в голове, вместо стандартного "не знаю, это далеко не моя область".

Не, ну я понимаю, конечно, что многого не понимаю, но... я ведь всего лишь искал некое приемлемое сравнение, ни в коем случае не претендуя на его абсолютную точность. Всякое сравнение хромает!

Вопрос об истинности или ложности континуум-гипотезы не перестаёт быть осмысленным, но вылетает, если можно так выразиться, из математической в метафизическую плоскость... Над ним можно долго размышлять... Математик может установить, что он выходит за рамки ZFC, но... сама ZFC ведь не на пустом месте появилась! Не знаю пока, как лучше об этом написать, надо будет подумать.

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

-- Ср сен 19, 2012 22:33:24 --

Munin в сообщении #621119 писал(а):

В геометрии Евклида Пятый постулат истинен, в геометрии Лобачевского - ложен. "Следует добавить" тоже неправильно: следует добавить, если мы хотим получить геометрию Евклида, а если мы хотим чего-то другого, то напротив, не следует добавлять.

А что нам следует делать, если мы хотим развить тригонометрию вкупе с теорией подобия треугольников, чтобы измерять расстояния до объектов на противоположной стороне реки, не переплывая реку?

-- Ср сен 19, 2012 22:38:46 --

Munin в сообщении #621119 писал(а):

Это что-то значит, или равносильно?

Со стопроцентной уверенностью сейчас не скажу, но, по-моему, равносильно.

Существенные отличия ищите там, где отрицания. Там есть разные формулировки системы аксиом: Гильберта, Лукашевича, ещё кого-то... Вот они в рамках одного типа исчисления эквивалентны. И везде, где написано "интуиционистское", не доказуемо $\Phi \vee \neg\Phi$ и $\neg\neg\Phi \rightarrow \Phi$. А в классическом варианте эти вещи доказуемы.

[epros]

Munin в сообщении #621031 писал(а):

С тем, что вы не можете внятно объяснить каких-то простых вещей, я уже сталкивался. Подожду, что Профессор Снэйп на мой вопрос ответит.

Может вопрос тогда постараетесь более внятно формулировать? Я же сказал, что к конечно-значной алгебре конструктивную логику свести нельзя. Это часть ответа и на этот вопрос:

Munin в сообщении #621102 писал(а):

Какие получаются законы алгебры логики, и законы работы с кванторами? Можно ли обойтись в минимальном варианте алгебры логики по-прежнему двумя значениями $\{0,1\},$ или приходится вводить какие-то ещё?

Более подробный ответ можно найти в статье англопедии Heyting algebra.

Профессор Снэйп в сообщении #621068 писал(а):

А истинно... вот он мальчик на улице, с ребятами футбол гоняет, а вот его пустая тетрадь, все желающие могут посмотреть и убедиться!!!

Хе, хе, хе. Вот какую вещь классические логики не могут понять: Что «посмотреть и убедиться» — это тоже способ доказательства. Причём при формальном описании он представляется тем самым «выводом в рамках теории».

Профессор Снэйп в сообщении #621068 писал(а):

В этом смысле закон исключённого третьего … для конструктивиста ложен

Это существенная неточность. Он не ложен, его просто нет в аксиоматике. Отрицать закон исключённого третьего невозможно, ибо это равносильно утверждению противоречия.

Munin в сообщении #621102 писал(а):

Это наиболее феерическая для меня часть истории. Как если бы один математик был убеждённым евклидовцем, а другой - убеждённым лобачевцем. Очевидно же, что при работоспособности двух систем можно свободно пользоваться обеими, оговаривая изначально, о чём речь.

Здесь то же самое — разница только в аксиоматиках. Для конструктивиста закон исключённого третьего — это такая же неочевидная и нетривиальная аксиома, как гипотеза континуума.

[Munin]

Профессор Снэйп в сообщении #621113 писал(а):

Не, ну чисто из соображений экономии мышления, если удобно.

Вот уж чего-чего, а экономия мышления для математиков, которые всю жизнь только тем и занимаются, что мышлением впустую! :-)

Профессор Снэйп в сообщении #621113 писал(а):

Это как отношение евклидовой и неевклидовой геометрий к физике.

Я бы согласился, но математика - это же не физика!

Профессор Снэйп в сообщении #621113 писал(а):

И та, и другая модель внутренне непротиворечивы и погружаются одна в другую, но вопрос о том, в какой модели мы реально живём, лежит в несколько иной плоскости.

Разве для математиков имеет хоть какое-то значение, где мы реально живём? Для меня очевидно, что мы вообще не живём ни в одной из перечисленных моделей. Для начала, любое доказательство можно написать и прочитать только в мечтах: в реальности мы ограничены длительностью человеческой жизни, и доказательство, требующее только для прочтения 200 лет (или $10^{10^{10}}$), не имеет шанса ни быть выведенным, ни проверенным. (Кстати, мне на это указал С. Лем, в "Экстелопедии Вестранда". Заодно, там же он предсказал Википедию :-)

Профессор Снэйп в сообщении #621113 писал(а):

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

Да неужто? Кто ему мешает свободно переходить от одной к другой, и писать работы и там и там?

Не понимаю этого, столь упёртого убеждения, что должна быть только одна master модель, оно столь неестествнно в физике, и столь широко распространено всюду за её пределами... уж где не ожидал его увидеть, так в математике.

Профессор Снэйп в сообщении #621113 писал(а):

У конструктивистов и интуиционистов появляются дополнительные аргументы метафизического плана.

Ну, верчение пальцами в воздухе - это аргументы скорее на уровне разговора на кухне с неспециалистами, или для выбора темы диссертации (это перспективно, а то - не очень). Интересно уши развесить, но ломаного гроша стоит.

[Профессор Снэйп]

epros в сообщении #621122 писал(а):

Более подробный ответ можно найти в статье англопедии Heyting algebra.

Да, кстати! Для классической логики булева алгебра, для интуиционистской гейтингова алгебра. Совсем из головы вылетело

-- Ср сен 19, 2012 22:50:00 --

epros в сообщении #621122 писал(а):

Хе, хе, хе. Вот какую вещь классические логики не могут понять: Что «посмотреть и убедиться» — это тоже способ доказательства. Причём при формальном описании он представляется тем самым «выводом в рамках теории».

А вот этот свой пресловутый "принцип конструктивного подбора" вы, конструктивисты, выводом в рамках какой теории обосновываете? Или повторяете, как заклинание, вслед за А. А. Марковым: "Посмотри на натуральный ряд и узри воочию"?

[Munin]

Профессор Снэйп в сообщении #621120 писал(а):

Вопрос об истинности или ложности континуум-гипотезы не перестаёт быть осмысленным, но вылетает, если можно так выразиться, из математической в метафизическую плоскость... Над ним можно долго размышлять... Математик может установить, что он выходит за рамки ZFC, но... сама ZFC ведь не на пустом месте появилась! Не знаю пока, как лучше об этом написать, надо будет подумать.

По-моему, всё, что "вылетает в метафизическую плоскость", вылетает из науки вообще. Пинком под зад. А Коэн как раз доказал, что не вылетает, за что ему честь и хвала.

Профессор Снэйп в сообщении #621120 писал(а):

А что нам следует делать, если мы хотим развить тригонометрию вкупе с теорией подобия треугольников, чтобы измерять расстояния до объектов на противоположной стороне реки, не переплывая реку?

Что делать? Изучать соответствие мысленных конструкций (Евклида и Лобачевского) и реальных объектов, расстояний и реки. Кстати, до Римана и Эйнштейна считали, что это соответствие однозначно указывает на Евклида (как бы там Лобачевский ни выпендривался), а потом оказалось, что вопрос ещё не решённый.

Профессор Снэйп в сообщении #621120 писал(а):

Существенные отличия ищите там, где отрицания. Там есть разные формулировки системы аксиом: Гильберта, Лукашевича, ещё кого-то... Вот они в рамках одного типа исчисления эквивалентны. И везде, где написано "интуиционистское", не доказуемо $\Phi \vee \neg\Phi$ и $\neg\neg\Phi \rightarrow \Phi$. А в классическом варианте эти вещи доказуемы.

epros в сообщении #621122 писал(а):

Более подробный ответ можно найти в статье англопедии Heyting algebra.

А, ага, спасибо!

epros в сообщении #621122 писал(а):

Я же сказал, что к конечно-значной алгебре конструктивную логику свести нельзя.

Видимо, вы это сказали как-то тихо или в сторону, так что я не расслышал.

epros в сообщении #621122 писал(а):

Здесь то же самое — разница только в аксиоматиках. Для конструктивиста закон исключённого третьего — это такая же неочевидная и нетривиальная аксиома, как гипотеза континуума.

Рад такое услышать. Но где обобщающая теория?