Конструктивная логика, матанализ и проч. (продолжение)

[epros]

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

Someone писал(а):

Напомню, что вопрос был следующий:

Someone в сообщении #142686 писал(а):
Вы отрицаете полезность математического анализа и основанных на нём областей математики?

Вы считаете, что Ваше
epros в сообщении #143246 писал(а):
конструктивный матанализ ничуть не хуже классического

является ответом на мой вопрос?

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

Это ответ?

Someone писал(а):

Someone писал(а):

Для аксиомы бесконечности таковой процедуры построить пока никому не удалось. Точнее, всё, что удаётся построить, оказывается без точки останова.

А что, кто-нибудь пытался? Ссылочку, пожалуйста, предъявите

Смеётесь? Вы хотите получить от меня ссылку на статью, где опубликован отчёт о неполучении математического результата? Конструктивные математики (начиная с Маркова) всегда начинали с признания, что не понимают, что такое актуальная бесконечность (а поэтому говорить о ней больше не будут). Что Вы ещё от них хотите? 500 страниц текста с описанием безуспешных попыток определения процедуры построения бесконечного множества?

Someone писал(а):

Теория ZF, в которой аксиома бесконечности заменена её отрицанием, эквивалентна арифметике Пеано. Называть арифметику Пеано тривиальной несколько рискованно

Вы не поняли. Никто не заменяет аксиому бесконечности её отрицанием. Это было бы столь же неконструктивно, как и принять её. Её (как и её отрицания) просто нет в аксиоматике.

Someone писал(а):

И если, по Вашему мнению, множество КДЧ конечно, то о какой эффективной несчётности говорит Б.А.Кушнер?

Я не говорил о конечности множества КДЧ! Ваша точка зрения настолько далека от конструктивизма, что похоже на то, что мы говорим на разных языках. Я сказал: "Без аксиомы бесконечности несомненно существующими оказываются только конечные множества". А Вы услышали утверждение о том, что бесконечных множеств не существует. Это не классическая двузначная логика. Если говорится, что мы не можем утверждать существование $X$, то это не означает утверждение о его несуществовании.

Понятие "множество всех КДЧ", насколько я знаю, просто неопределимо: не придумано процедуры, которая бы сгенерировала их все.

Someone писал(а):

Всё ясно. Б.А.Кушнер - вражеский агент в стане конструктивистов

Не ожидал услышать от Вас аргументацию на таком уровне: когда высмеивается то, чего я не говорил.

Someone писал(а):

Совершенная чушь. Вы попросту не знаете и не понимаете того, что пытаетесь здесь отстаивать и пропагандировать. Логика у конструктивистов отличается от классической, аристотелевой логики, но, тем не менее, является такой же двузначной: всякое высказывание либо истинно, либо ложно. Основное отличие от классической логики состоит в том, что в классической логике обязательно истинно в точности одно из двух высказываний $A$ и $\neg A$ (закон исключённого третьего), в то время как в конструктивистской логике оба этих высказывания могут оказаться ложными, а высказывание $\neg \neg A$ может не совпадать с $A$ (но $\neg \neg \neg A = \neg A$). Есть также некоторые другие отличия.

Может я чего-то и не знаю или не понимаю, но я ожидал услышать от Вас возражения по существу, а не рассуждения о моей компетентности. И это при том, что Ваши утверждения, как мне кажется, не свидетельствуют о хорошем понимании Вами данного предмета: "Всякое высказывание либо истинно, либо ложно" - это утверждение, будучи формализованным, влечёт за собой всю классическую логику (исчисление высказываний), включая законы исключённого третьего и снятия двойного отрицания. А Вы приписываете его, в том числе, конструктивной логике, в которой этих законов нет. "В конструктивистской логике оба этих высказывания могут оказаться ложными" - это просто не так. Утверждение $\neg \neg A \land \neg A$ представляет собой тождественную ложь, т.е. не при каких условиях не может возникнуть такой ситуации, о которой Вы говорите.

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

[luitzen]

epros писал(а):

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

Смотря что за теория… Вот попробуйте интуиционистски доказать формулу логики предикатов первого порядка $\neg\neg (\forall x \neg\neg A(x) \to \neg\neg \forall x A(x))$.

[epros]

luitzen писал(а):

Смотря что за теория… Вот попробуйте интуиционистски доказать формулу логики предикатов первого порядка $\neg\neg (\forall x \neg\neg A(x) \to \neg\neg \forall x A(x))$.

Может быть $\neg\neg (\neg\neg \forall x A(x) \to \forall x \neg\neg A(x))$?

А то, вроде бы, из $\forall x \neg\neg A(x)$ выводится $\neg \exists x \neg A(x)$, а из него выводится $\neg\neg \forall x A(x)$ и таким образом импликация внутри скобок доказывается, а значит и двойное отрицание от неё.

Но вообще-то интересно. Если и правда не выводится, то как быть с пресловутой теоремой Гливенко?

[luitzen]

epros писал(а):

Может быть $\neg\neg (\neg\neg \forall x A(x) \to \forall x \neg\neg A(x))$?

А то, вроде бы, из $\forall x \neg\neg A(x)$ выводится $\neg \exists x \neg A(x)$, а из него выводится $\neg\neg \forall x A(x)$ и таким образом импликация внутри скобок доказывается, а значит и двойное отрицание от неё.

У Клини во «Введении в метаматематику» на с. 151 есть таблица на эту тему. Доказывается же всё это в теореме 58 (сс. 430–434).

Цитата:

Если и правда не выводится, то как быть с пресловутой теоремой Гливенко?

Теорема Гливенко сформулирована применительно к пропозициональной логике.

[Someone]

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

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

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

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

epros писал(а):

Отсюда и впечатление о нём как о какой-то жалкой пародии на классическую логику.

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

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

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

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

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

Смеётесь? Вы хотите получить от меня ссылку на статью, где опубликован отчёт о неполучении математического результата?

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

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

Что Вы ещё от них хотите? 500 страниц текста с описанием безуспешных попыток определения процедуры построения бесконечного множества?

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

И не открещивайтесь от аксиомы бесконечности. Формально в конструктивной математике её нет, но замена имеется. Конструктивная математика вовсю эксплуатирует множество слов (в алфавите, используемом алгоритмами), которое бесконечно. Будем ли мы его при этом считать "актуально бесконечным" или "потенциально бесконечным" - вопрос философский, а не математический.

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

Вы не поняли. Никто не заменяет аксиому бесконечности её отрицанием.

Вы написали так:

epros писал(а):

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

Я объяснил, что на самом деле теория получается отнюдь не тривиальная.

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

Не ожидал услышать от Вас аргументацию на таком уровне: когда высмеивается то, чего я не говорил.

Я приведу Ваш текст:

epros писал(а):

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

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

А почему кто-то может волноваться из-за отсутствия несчётных (в классическом смысле) множеств в конструктивном анализе, понять вообще нельзя.

И не верю я, что такое сильное утверждение, как неперечислимость множества КДЧ, может не иметь никаких полезных следствий. Я привык не делать подобных заявлений.

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

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

Нет, Вы забываете, что в конструктивной логике другое отрицание, чем в классической. Если в классической логике истинность $\neg A$ означает, что $A$ ложно, то в конструктивной истинность $\neg A$ означает, что $A$ можно привести к противоречию. Вполне может так случиться, что $A$ ложно, но построить противоречие, используя $A$, в конструктивной логике нельзя. Тогда $\neg A$ тоже будет ложно.
Не забывайте также, что истинность и ложность - это всего лишь значения оценочной функции на множестве высказываний. Эта оценочная функция определённым образом связана с аксиомами (логическими и нелогическими) и правилами вывода, но выводимость высказывания зависит от набора этих самых аксиом и правил вывода и, вообще говоря, не всякое истинное (в смысле оценочной функции) высказывание выводится из аксиом посредством принятых правил вывода.
Также никто не запрещает использовать более чем двузначную оценочную функцию, если уж Вам этого хочется.

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

Утверждение $\neg\neg A\land\neg A$ представляет собой тождественную ложь

Не отрицаю.

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

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

А здесь Вы опять путаете конструктивное отрицание с классическим.

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

Вот только они забывают про два момента:

Вы не могли бы не высказываться за других? Откуда Вы знаете, что они забывают, а что - нет?

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

А есть масса вещей, которые при всей их неопровержимости нет никаких оснований считать истинными

Ещё раз: не путайте истинность и выводимость.

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

Понятие "множество всех КДЧ", насколько я знаю, просто неопределимо: не придумано процедуры, которая бы сгенерировала их все.

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

[epros]

luitzen писал(а):

У Клини во «Введении в метаматематику» на с. 151 есть таблица на эту тему. Доказывается же всё это в теореме 58 (сс. 430–434).

Любопытно. Книжка Клини мне в данный момент недоступна, попробую добыть...

luitzen писал(а):

Теорема Гливенко сформулирована применительно к пропозициональной логике.

Ага, понятно.

Добавлено спустя 2 часа 53 минуты 9 секунд:

Someone писал(а):

Поскольку термин "математический анализ" существует очень давно, гораздо (в разы) дольше, чем "конструктивный математический анализ", он означает именно классический математический анализ.

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

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

Someone писал(а):

отрицаете ли Вы полезность математического анализа, "основанного" на аксиоме бесконечности?

Нет, не отрицаю. Я отрицаю полезность аксиомы бесконечности в матанализе. Ибо как показала практика последователей Брауэра, развивавших "существовавший очень давно" матанализ без использования аксиомы бесконечности, получается штука не менее полезная, чем с аксиомой бесконечности.

Someone писал(а):

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

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

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

Вопрос о существовании актуальной бесконечности - это не философия, а математика, ибо он может быть формализован в языке логики первого порядка в виде утверждения о существовании индуктивного множества. Но для конструктивистов такое утверждение неприемлемо, поскольку любое утверждение о существовании должно предполагать процедуру построения соответствующего объекта: предъявИте процедуру, будет о чём говорить (примерно в этом и заключается позиция Маркова).

Someone писал(а):

Могла бы быть теорема типа "не существует алгоритма, проверяющего (в точно определённом смысле) аксиому бесконечности".

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

Someone писал(а):

Без этого Ваше утверждение является бессмысленным.

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

Someone писал(а):

Философствования на тему предварительной проверки (в весьма неопределённом смысле) аксиом перед их принятием относятся совсем не к математике. Конструктивность, кстати сказать, понимается в весьма разных смыслах.

Только не самими конструктивистами! Конструктивисты понимают её в строгом формализуемом смысле. Поэтому те, кто понимают "конструктивность" в философском смысле, т.е., например, безоговорочно принимают аксиому бесконечности, но "сомневаются в конструктивности" аксиомы выбора, - это не конструктивисты.

Someone писал(а):

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

Нет, это любая исполнимая процедура, результатом которой является соответствующее множество в том или ином представлении. Математика оперирует только со строками символов, значит в рамках математики представлением множества должна быть некая строка символов. Это значит, что Вы имеете право строить множество не только "по одному элементу", а например, по десять (если определите процедуру добавления 10-ти элементов). Или, если хотите, можете определить процедуру добавления по 10 элементов, через которую определите процедуру добавления по 10^10 элементов, через которую определите процедуру добавления по 10^10^10 элементов... Но в итоге должна получиться процедура с конечным описанием, имеющая точку останова, в которой она предъявит Вам в качестве результата искомое множество.

Someone писал(а):

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

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

Someone писал(а):

И не открещивайтесь от аксиомы бесконечности. Формально в конструктивной математике её нет, но замена имеется. Конструктивная математика вовсю эксплуатирует множество слов (в алфавите, используемом алгоритмами), которое бесконечно. Будем ли мы его при этом считать "актуально бесконечным" или "потенциально бесконечным" - вопрос философский, а не математический.

Конструктивная математика использует слова в алфавите, но она не пытается измерить их количество или собрать их все во множество. Если с классической точки зрения все объекты, с которыми мы когда-нибудь будем иметь дело, в логическом смысле "существуют изначально" (отсюда и попытки обобщённо говорить о всём том, с чем мы ещё не имели дело), то с конструктивной точки зрения объекты создаются, т.е. "конструируются". Сконструировали - значит объект существует. Не сконструировали - значит и говорить пока не о чем.

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

Someone писал(а):

Поскольку Б.А.Кушнер говорит как раз о том, что Вы считаете происками "классицистов", и, более того, уделяет этому достаточно большое внимание, мне остаётся сделать вывод, что Вы его относите к вражеским агентам.

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

Someone писал(а):

Успокойтесь, конструктивизм в Вашей защите не нуждается.

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

Someone писал(а):

И не верю я, что такое сильное утверждение, как неперечислимость множества КДЧ, может не иметь никаких полезных следствий. Я привык не делать подобных заявлений.

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

Someone писал(а):

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

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

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

Я не знаю, откуда Вы взяли такую "конструктивную" интерпретацию понятия "ложно". Приведение к противоречию и является доказательством ложности утверждения, оно же - доказательство отрицания. Другое дело, что понятие "ложности" не является противоположностью (единственной альтернативой) понятию "истинности". То, о чём Вы говорите как о "ложном" (т.е. "не истинном"), кажется, у Гейтинга называется "слабым отрицанием". Каковое, собственно, и отрицанием-то не является, а представляет собой просто отсутствие утверждения.

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

Добавление. Чтобы нам с Вами впустую не спорить относительно того, сколько в конструктивной логике логических значений, загляните в: Новиков "Конструктивная математическая логика с точки зрения классической". Гл.2, п.5, теоремы 2 и 3.

Someone писал(а):

Вполне может так случиться, что $A$ ложно, но построить противоречие, используя $A$, в конструктивной логике нельзя. Тогда $\neg A$ тоже будет ложно.

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

Someone писал(а):

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

Я знаком с этой (классической) точкой зрения. Вы ещё не построили конкретной формулы для оценочной функции, а уже утверждаете, что она "существует" и даже декларируете наличие у неё определённых свойств (в частности - наличие строго определённого множества значений, например - двух). Хочу Вам заметить, что в конструктивизме всё не так: для конструктивного анализа "оценочной функцией" является сама процедура вывода в теории. Впрочем, Вы имеете право определить любую "оценочную функцию" (только не забывайте, что "определить" - значит "построить процедуру вычисления логического значения для заданной строки утверждения"). В таком случае процедура вычисления логического значения + проверка того, что оно = "истинно", - это и будет процедурой доказательства, т.е. в итоге мы получим "теорию".

Someone писал(а):

Ещё раз: не путайте истинность и выводимость.

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

Someone писал(а):

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

Понятие "множество всех КДЧ", насколько я знаю, просто неопределимо: не придумано процедуры, которая бы сгенерировала их все.

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

Нет, не путаю. Я говорю об определении, а не о перечислении. Я не сказал "все по очереди". Процедура, которая должна определить "множество всех КДЧ", должна предъявить в качестве результата математический объект (строку), из которой с помощью операции "принадлежит к" извлекается любое КДЧ.

[вздымщик Цыпа]

Я так понял, речь идет о двух не очень связанных между собой вещах:

1) (логическая) Схема аксиом $\neg\neg A \supset A$ заменяется на $A\supset (\neg A \supset B)$, что приводит к невыводимости $A \vee \neg A$ .

2) (теоретико-множественная) Аксиома $\exists \omega \,(\varnothing \in \omega \mathbin{\&} (x\in \omega \supset x \cup \{x\} \in \omega))$ удаляется.

Смысл второго мне понятен (ну или мне кажется, что понятен), но вот в чем смысл первого? Ведь в любой конечной модели (а других быть уже не может) для каждой формулы $P(x_1,\ldots,x_n)$ может быть установлено $P(\ldots)$ или $\neg P(\ldots)$, верно ведь? Так зачем модифицируется и логика тоже?

[epros]

вздымщик Цыпа писал(а):

1) (логическая) Схема аксиом $\neg\neg A \supset A$ заменяется на $A\supset (\neg A \supset B)$, что приводит к невыводимости $A \vee \neg A$.

Не совсем "заменяется", поскольку закон $A \to (\neg A \to B)$ есть не только в конструктивной логике, но и в классической. Скорее речь идёт о том, что закон снятия двойного отрицания просто отменяется. Кстати, есть варианты интуиционистской логики без закона $A \to (\neg A \to B)$, который считается просто "доопределением импликации".

вздымщик Цыпа писал(а):

но вот в чем смысл первого? Ведь в любой конечной модели (а других быть уже не может) для каждой формулы $P(x_1,\ldots,x_n)$ может быть установлено $P(\ldots)$ или $\neg P(\ldots)$, верно ведь? Так зачем модифицируется и логика тоже?

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

Да, вот первый же подвернувшийся пример из книжки Гейтинга "Интуиционизм".


В терминах процедур: Если $X$ - процедура проверки того, что число $\rho$ рационально, то она не может не иметь точки останова (даже если $\rho=1/3$), но где эта точка - никому не ведомо.

[вздымщик Цыпа]

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

Не совсем "заменяется", поскольку закон $A \to (\neg A \to B)$ есть не только в конструктивной логике, но и в классической. Скорее речь идёт о том, что закон снятия двойного отрицания просто отменяется.

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

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

утверждение об отсутствии конечной модели для конструктивной логики - это классическая теорема

Но это следствие модификации. Мне же непонятна причина.

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

конструктивизм не занимается такой ерундой, как построение моделей для собственной логики

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

[epros]

вздымщик Цыпа писал(а):

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

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

[вздымщик Цыпа]

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

терминах процедур: Если $X$ - процедура проверки того, что число $\rho$ рационально, то она не может не иметь точки останова (даже если $\rho=1/3$), но где эта точка - никому не ведомо.

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

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

Непонятно, но занятно Ладно, попробую почитать, может прояснится. Извините за беспокойство.

[Someone]

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

...

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

P.S. А что касается классического математического анализа, то забудьте о философствованиях и скажите, какие конкретно результаты, полученные математиками в XVIII и XIX веках, были отвергнуты в результате применения теоретико-множественного подхода. Если не сможете, подумайте, чего стóит Ваше утверждение на эту тему с точки зрения конструктивной логики.

[epros]

вздымщик Цыпа писал(а):

Непонятно, но занятно Ладно, попробую почитать, может прояснится. Извините за беспокойство.

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

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

Добавлено спустя 20 минут 8 секунд:

Someone писал(а):

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

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

Someone писал(а):

P.S. А что касается классического математического анализа, то забудьте о философствованиях и скажите, какие конкретно результаты, полученные математиками в XVIII и XIX веках, были отвергнуты в результате применения теоретико-множественного подхода. Если не сможете, подумайте, чего стóит Ваше утверждение на эту тему с точки зрения конструктивной логики.

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

[Someone]

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

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

Не говорите ерунду. Новая теория (в данном случае - теория множеств) является "основанием" классического математического анализа в том смысле, что в ней формализуются все построения и рассуждения, применявшиеся в нём до появления теории множеств. Ничего из того, что было "добыто" в математическом анализе до теории множеств, не отбрасывается. Если же отказаться от аксиомы бесконечности, то теория множеств не сможет выполнять эту функцию. Между тем, она именно ради этой цели и строилась. Хотя явно сформулированной аксиомы бесконечности до появления аксиоматической теории множеств не было, но построения, на ней основанные, всегда были.

Вообще, постарайтесь хотя бы понять, что термины "классическая математическая логика" и "классический математический анализ" не могли появиться до разработки их неклассических аналогов, поскольку в таких терминах не было надобности. А вот когда появились интуиционизм и конструктивизм, существовавшее до того направление получило название классического. Поэтому математический анализ, существовавший в XVIII-XIX веках, и есть классический математический анализ, а использовавшаяся в нём логика - классическая математическая логика.

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

Если бы физика стояла на такой позиции, то мы бы сейчас копались в уточнениях Птолемеевской модели Вселенной.

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

Вообще, физика не отвергает теории, которые хорошо работают в своей области. Классическая механика не исчезла после появления СТО и квантовой механики. Ньютоновский закон всемирного тяготения и СТО не исчезли после появления ОТО. Термодинамика не исчезла после появления статистической физики.

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

Брауэр отверг Аристотелевский закон исключённого третьего, на что "классические" математики не решились. Ну и что? Этот закон был в своё время с потолка взят (как и "абсолютность времени" в физике, например). Берём бритву Оккама и нещадно режем...

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

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

Упоминание "предшествующего опыта" - это намёк на мою тупость?

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

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

Добавление. Чтобы нам с Вами впустую не спорить относительно того, сколько в конструктивной логике логических значений, загляните в: Новиков "Конструктивная математическая логика с точки зрения классической". Гл.2, п.5, теоремы 2 и 3.

Если внимательно почитать Новикова, то можно обнаружить, что он упоминает любое конечное $\geqslant 2$, а также счётное число логических значений.

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

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

Someone в сообщении #144869 писал(а):

И не верю я, что такое сильное утверждение, как неперечислимость множества КДЧ, может не иметь никаких полезных следствий. Я привык не делать подобных заявлений.

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

Видите ли, Вы претендуете на то, что конструктивизм может быть такой же (не худшей) основой математического анализа, что и теория множеств с классической логикой. В математическом анализе несчётность множества действительных чисел существенна для построения меры Лебега и интеграла Лебега. Насколько я знаю, соответствующие понятия в конструктивном анализе есть. Для них также существенной должна быть эффективная несчётность (= неперечислимость) множества КДЧ.

И ещё, совсем не обязательно интерпретировать множество как совокупность объектов. Просто такая интерпретация наглядна и удобна. Но можно интерпретировать множества как свойства. У Кушнера можно найти упоминание о том, что в конструктивной теории множества именно так и интерпретируются.

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

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

Не имею желания дискутировать на тему "что лучше: классический анализ или конструктивный". Такая дискуссия бессмысленна. Я дал некоторые разъяснения, но от дальнейшей дискуссии устраняюсь. Думаю, что нетрудно найти на форуме тех, кто мог бы представлять классическую математику на более высоком уровне, но захотят ли они участвовать в такой дискуссии, не знаю.

[luitzen]

Someone писал(а):

Поэтому математический анализ, существовавший в XVIII-XIX веках, и есть классический математический анализ, а использовавшаяся в нём логика - классическая математическая логика.

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

Someone писал(а):

Если внимательно почитать Новикова, то можно обнаружить, что он упоминает любое конечное $\geqslant 2$, а также счётное число логических значений.

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

Someone писал(а):

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

У меня, наоборот, сложилось впечатление, что хорошим тоном является доказывать разные хорошие свойства классической логики и основанных на ней теорий как можно более конструктивными методами. То есть, Ваше замечание в скобках я бы переписал так: «но, кажется, самим конструктивистам пока не до этого».

Someone писал(а):

Нет, Вы забываете, что в конструктивной логике другое отрицание, чем в классической. Если в классической логике истинность $\neg A$ означает, что $A$ ложно, то в конструктивной истинность $\neg A$ означает, что $A$ можно привести к противоречию. Вполне может так случиться, что $A$ ложно, но построить противоречие, используя $A$, в конструктивной логике нельзя. Тогда $\neg A$ тоже будет ложно.
Не забывайте также, что истинность и ложность — это всего лишь…

Это звучит непохоже на всё то, что я слышал, и, следовательно, попахивает ересью. Не могли бы Вы, Someone, привести какой-то конкретный пример такого высказывания $A$? Иначе создаётся впечатление, что Вы сами пытаетесь натянуть на конструктивную логику эту самую двузначную оценочную функцию.