Интуиционистская логика. В чем проблема?

[bayah]

Здравствуйте. Слушал лекцию про логику, узнал о Брауэре и интуиционистской логике. А именно, речь шла о критике закона исключения третьего.
Википедия (https://ru.wikipedia.org/wiki/%D0%97%D0 ... 0%B3%D0%BE) приводит пример:

Цитата:

Гораздо более тонкий пример применения закона исключённого третьего, который хорошо демонстрирует, почему он не является приемлемым с точки зрения интуиционизма, состоит в следующем. Предположим, что мы хотим доказать теорему, что существуют иррациональные числа a и b, такие что $a^b$ рационально. Известно, что $\sqrt{2}$ иррационально. Рассмотрим $\sqrt{2}^{\sqrt{2}}$. Если данное число рационально, то теорема доказана.
Иначе возьмём $a=\sqrt{2}^{\sqrt{2}} и b=\sqrt{2}$.
Тогда

$$a^b = \left(\sqrt{2}^{\sqrt{2}}\right)^{\sqrt{2}} = \sqrt{2}^{\left(\sqrt{2}\cdot\sqrt{2}\right)} = \sqrt{2}^2 = 2,$$

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

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

[Kras]

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

bayah в сообщении #1023869 писал(а):

Рассмотрим $\sqrt{2}^{\sqrt{2}}$. Если данное число рационально, то теорема доказана.

Здесь мы ничего не можем сказать о числе $\sqrt{2}^{\sqrt{2}}$, является оно рациональным или иррациональным. Из доказательства невозможно понять, на каком этапе мы приходим к нужному результату.
Между тем, кажется, из некоторых результатов Гельфонда следует, что число $\sqrt{2}^{\sqrt{2}}$ является иррациональным.

[whitefox]

bayah в сообщении #1023869 писал(а):

Скажите, это верное доказательство? Можно так делать в математике? И вообще, можете объяснить, почему тут закон исключения третьего неприменим?

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

[bayah]

Kras в сообщении #1023873 писал(а):

Здесь мы ничего не можем сказать о числе $\sqrt{2}^{\sqrt{2}}$, является оно рациональным или иррациональным. Из доказательства невозможно понять, на каком этапе мы приходим к нужному результату.
Между тем, кажется, из некоторых результатов Гельфонда следует, что число $\sqrt{2}^{\sqrt{2}}$ является иррациональным.

Ну да, но тут же мы вроде бы доказываем просто существование таких чисел. С этим же все в порядке?
Доказательство рациональности или иррациональности $\sqrt{2}^{\sqrt{2}}$ это уже другое доказательство.

whitefox в сообщении #1023884 писал(а):

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

А простите, тогда какая математика используется математиками сейчас?)
И в чем именно смысл такой критики закона исключения третьего? Для чего интуиционистская логика нужна?

[Kras]

bayah в сообщении #1023888 писал(а):

Ну да, но тут же мы вроде бы доказываем просто существование таких чисел. С этим же все в порядке?

Разумеется все в порядке. Проблемы начнутся, если мы зададимся вопросом, а что взять в качестве $a$ и $b$...

bayah в сообщении #1023888 писал(а):

Доказательство рациональности или иррациональности $\sqrt{2}^{\sqrt{2}}$ это уже другое доказательство.

Нет, это то же самое доказательство. Если найти конкретный пример, то вопрос о существовании снимается сразу.

bayah в сообщении #1023888 писал(а):

И в чем именно смысл такой критики закона исключения третьего? Для чего интуиционистская логика нужна?

Думаю, весь смысл и вся польза состоит в построении конкретных объектов.

[bayah]

Kras в сообщении #1023892 писал(а):

Нет, это то же самое доказательство. Если найти конкретный пример, то вопрос о существовании снимается сразу.

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

Kras в сообщении #1023892 писал(а):

Думаю, весь смысл и вся польза состоит в построении конкретных объектов.

То есть в интуиционистской логике требование доказывать только с построением конкретных примеров это просто дело "математического вкуса"?)

[whitefox]

bayah в сообщении #1023888 писал(а):

А простите, тогда какая математика используется математиками сейчас?)

Ещё можно спросить — а на каком языке математики пишут свои работы сейчас?
Ответ — и та, и другая, и третья, . . .
Но, по большей части, классическая.

Гильберт писал(а):

Никто не может изгнать нас из рая созданного нам Кантором!

bayah в сообщении #1023888 писал(а):

И в чем именно смысл такой критики закона исключения третьего? Для чего интуиционистская логика нужна?

Эта одна из попыток преодолеть антиномии теории множеств.

-- 06 июн 2015, 10:35 --

bayah в сообщении #1023893 писал(а):

То есть в интуиционистской логике требование доказывать только с построением конкретных примеров это просто дело "математического вкуса"?)

Воспринимайте это как игру по ограниченному списку правил. Подобно тому как в античности многие увлекались решением геометрических задач на построение только при помощи циркуля и линейки. Этакая игра разума.

[Kras]

bayah в сообщении #1023893 писал(а):

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

Получается так. Во втором случае мы обнаруживаем не только сам факт существования хотя бы одной пары чисел, но и конкретную пару чисел:) В первом же случае мы устанавливаем только существование и ничего больше.

[bayah]

Ну кое что прояснилось в моей голове.
Всем спасибо)

[epros]

bayah в сообщении #1023888 писал(а):

А простите, тогда какая математика используется математиками сейчас?)

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

bayah в сообщении #1023888 писал(а):

И в чем именно смысл такой критики закона исключения третьего?

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

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

bayah в сообщении #1023888 писал(а):

Для чего интуиционистская логика нужна?

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

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

[bayah]

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

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

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

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

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

То есть в интуиционистской логике истинным признается только то что доказано? А как может быть иначе и каким образом на это влияет закон исключенного третьего?
А можете привести пример, где ясна истинность высказывания, но которую невозможно доказать?
И как вообще тогда возможно полагать что-то истинным?

[Xaositect]

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

Действительное число может быть как-то связано с каким-то утверждением на натуральных числах. Допустим, у нас есть $x = \sum_{k = 0}^\infty 2^{-k} G(k)$, где $G(k)$ - верхний предел последовательности Гудстейна, начинающейся с $k$. Мы не можем ни доказать, ни опровергнуть утверждение $x=0$.

bayah в сообщении #1024343 писал(а):

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

Подвергаться сомнению может что угодно. Есть, например, логики, в которых подвергаются сомнению структурные правила, например, в которых из пары гипотезы $A, A$ может выводиться не то же самое, что из одной гипотезы $A$. Такая логика может использоваться в теориях типов с учетом ресурсов, используемых функциями.

[epros]

bayah в сообщении #1024343 писал(а):

А разве это аксиома?

$p \vee \neg p$, строго говоря, является схемой аксиом (т.е. для каждого высказывания $p$ это аксиома). См. гильбертовскую аксиоматизацию классической логики высказываний.

bayah в сообщении #1024343 писал(а):

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

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

bayah в сообщении #1024343 писал(а):

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

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

bayah в сообщении #1024343 писал(а):

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

Иначе может быть (и есть) в классической логике: Как я уже сказал, классическая логика вынуждена признавать существование недоказуемых истин. То, что недоказуемые и неопровержимые высказывания существуют в любой достаточно содержательной теории, утверждает первая теорема Гёделя о неполноте (и доказательство этого вполне конструктивно). А то, что каждое такое высказывание либо истинно, либо ложно, утверждает закон исключённого третьего. Причём независимо от того, истинно такое высказывание или ложно, у нас появляется недоказуемая истина.

bayah в сообщении #1024343 писал(а):

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

Не так. Могу привести пример высказывания, которое либо истинно, либо ложно независимо ни от какой прикладной аксиоматики. В первом случае оно является недоказуемой истиной, во втором случае недоказуемой истиной является его отрицание. А какой из двух случаев "в действительности" имеет место -- мы не знаем и, очевидно, никогда не узнаем.

Таковым высказыванием является континуум-гипотеза, которая на языке классической логики второго порядка может быть сформулирована без привлечения какой бы то ни было дополнительной аксиоматики (т.е. ни аксиомы арифметики, ни аксиомы теории множеств и т.д. не используются).

bayah в сообщении #1024343 писал(а):

И как вообще тогда возможно полагать что-то истинным?

Ещё раз: В классической логике истинность не привязана (и не может быть привязана) к доказуемости, поэтому "полагайте" как хотите. Например, в теории множеств Цемерло-Френкеля та же континуум гипотеза неопровержима и недоказуема, а это значит, что "полагать" её истинной или ложной Вы можете по своему усмотрению. Однако закон исключённого третьего говорит, что она "обязана" быть истинной или ложной, ибо логического значения "неразрешима" не существует.

-- Вс июн 07, 2015 15:17:03 --

Xaositect, извиняюсь, если в чём-то с Вами перекликаюсь: Ваше сообщение появилось пока я набирал своё.

[whitefox]

(Оффтоп)

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

Подвергаться сомнению может что угодно.

Xaositect в сообщении #1024362 писал(а):

Подвергаться сомнению может что угодно.

В том числе и само это утверждение.
В том числе и утверждение в предыдущей строке.
. . .
и т.д.

[Anton_Peplov]

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

То, что недоказуемые и неопровержимые высказывания существуют в любой достаточно содержательной теории, утверждает первая теорема Гёделя о неполноте

В любой или в теории с перечислимым множеством аксиом?