Существует ли биекция между вычислимыми числами и нат.?

[ewert]

и всё-таки. Есть в конструктивной математике утверждение насчёт того, что каждое ограниченное множество имеет супремум?

[Nxx]

Нет, более того, есть контрпример.

[ewert]

хорошо, тогда пока -- более мягкий факт. Есть ли утверждение о том, что любая "непрерывная" функция ограничена?

(и, кстати, есть ли само понятие "непрерывности"? -- я как-то упустил из виду, обсуждалось ли это)

[Nxx]

А почитать слабо? Я сейчас читаю вышеприведенную книжку по конструктивному анализу и вам пересказываю. Вам нужен переводчик?

[ewert]

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

[Nxx]

ewert писал(а):

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

Вам жалко скачать 4 Мб?

[ewert]

Сию секунду это будет стоить 20 р. при сомнительной пользе. Лучше на трамвае прокачусь.

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

[маткиб]

Nxx в сообщении #186049 писал(а):

Полностью курс конструктивного анализа можно скачать тут:

http://www.krelib.com/files/math/Analis_Kush.djvu

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

Кстати, "не может не существовать" - это значит "существует" или же это очередное конструктивистское извращение?

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

В подробностях не разбирался, ибо не понятно, ЗАЧЕМ

[Nxx]

Цитата:

В подробностях не разбирался, ибо не понятно, ЗАЧЕМ

Там во введении написано, зачем.

[epros]

маткиб писал(а):

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

Если есть возможность получить конкретное решение, то это можно сделать конструктивными методами.

Доказательство?

В следующем предложении: Следует из того, как конструктивисты понимают "конструктивность" методов.

маткиб писал(а):

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

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

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

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

маткиб писал(а):

Да и к аргументам о неудобности и увеличении объёма выкладок неохотно прислушиваются.

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

маткиб писал(а):

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

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

маткиб писал(а):

И зачем Вы это продемонстрировали? Оно что-то показывает?

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

маткиб писал(а):

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

Это когда Вы человеку предъявляете абстрактную формулировку. А если спросить, можно ли к строке чёрточек добавить чёрточку, то, по-моему, практически любому можно объяснить, что помешать этому могут только ограничения в бумаге или чернилах.

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

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

маткиб писал(а):

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

А в чём проблема с индукцией? Она определяется мета-теоретической аксиомой, которая говорит о "всех формулах арифметики". При этом, естественно, совершенно неважно, какие кванторы стоят в самой соответствующей "формуле арифметики".

Проблема в том, откуда она взялась. Например, пусть $P(n)$ выражает свойство "уравнение $x^{n+3}+y^{n+3}=z^{n+3}$ не имеет решений в натуральных числах". И если бы я был конструктивистом, то аксиома

$$ P(0)\&(\forall n)(P(n)\rightarrow P(n+1))\rightarrow (\forall n)P(n) $$

была бы для меня далеко не очевидна. Например, $P(n)\rightarrow P(n+1)$ может быть разрешимым и истинным для каждого конкретного $n$, но для его разрешения к каждому $n$ нужен индивидуальный (творческий) подход. Тогда не факт, что $(\forall n)P(n)$ будет разрешима.

Да, совершенно не факт.

Дело вот в чём. Когда Вы говорите: "$P(n)\rightarrow P(n+1)$ может быть разрешимым и истинным для каждого конкретного $n$", - то это означает ни что иное, как мета-теоретическое утверждение:
$(\forall n)(A \vdash P(n) \rightarrow P(n+1))$, где $A$ означает формальную арифметику.
Если Вы можете позволить себе такое утверждение в мета-теории, то у Вас, очевидно, есть тому какое-то доказательство (не смотря на индивидуальность и творческий характер подхода для каждого $n$). Но отсюда совершенно никак не следует вот это:
$A \vdash (\forall n)(P(n) \rightarrow P(n+1))$

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

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

маткиб писал(а):

Кстати, "не может не существовать" - это значит "существует" или же это очередное конструктивистское извращение?

Это "очередное конструктивистское извращение", а именно - двойное отрицание, которое не обязательно сводимо к утверждению. Например, определённое PAV действительное число x "не может не быть" рациональным. Но это не означает, что мы вправе утверждать, что оно "в любом случае рационально".

[ewert]

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

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

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

[Someone]

Nxx в сообщении #185766 писал(а):

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

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

Nxx в сообщении #185534 писал(а):

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

А за пределами RA понятия алгоритмической вычислимости нет. Я писал:

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

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

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

Nxx в сообщении #185766 писал(а):

Вообще-то, давно доказано, что задача останова нерешаема.

Да. Только в таких теоремах, насколько я знаю, речь идёт о бесконечной последовательности алгоритмов, а задачу останова требуется решать одним алгоритмом. А в обсуждаемой ситуации речь идёт о конечной последовательности алгоритмов.

Nxx в сообщении #185766 писал(а):

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

Стоп. Вы это второй раз повторяете, несмотря на моё объяснение. Почему это "единственный способ"? Вы хотя бы про принцип Маркова прочли? Он позволяет использовать запрещённые в CRA доказательства "от противного" для решения вопроса об остановке алгоритма. Здесь нет необходимости дожидаться остановки алгоритма. Тем более Ваше утверждение выглядит странным для классической математики в условиях, когда можно расширять арсенал используемых средств решения этого вопроса.

Nxx в сообщении #185832 писал(а):

Более того, согласно теореме Геделя, существуют алгоритмы, которые никогда не остановятся, но доказать это невозможно.

Странное утверждение. Откуда же тогда известно, что они не остановятся? В свете сказанного выше.

Nxx в сообщении #185766 писал(а):

Цитата:

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

Этим занимается теория сложности, которая еще больше приближает нас к реальному миру.

Не понял, причём тут теория сложности. Она что, отменяет физические ограничения на возможности физических устройств?

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

Someone писал(а):

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

Вот это логика! Я просто в шоке.
Т.е. он не имеет отношения "к наличию или отсутствию решения", но в то же время утверждает, что оно "либо есть, либо нет". А "есть" и "нет" это разве не "наличие" и "отсутствие" соответственно?

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

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

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

Перевираете. Вот цитата:

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

Для меня, например, закон исключённого третьего не очевиден по одной простой причине: Если задача достаточно сложная, так что уже многие поколения математиков + масса привлечённых вычислительных ресурсов не смогли её пока что решить, то не исключено, что эта задача никогда, никем и нигде не будет решена. Что равносильно отсутствию решения в принципе. А закон исключённог третьего зачем-то такую возможность исключает. Зачем? Или на основании чего?

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

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

Неужели так прямо и заявил, что "железно обоснован"?

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

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

Someone писал(а):

Цитата:

Ещё одно откровение. А кто-то недавно уверял меня, что интуитивных представлений о формально не определяемых строках более чем достаточно для надёжного обоснования CRA...

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

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

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

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

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

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

Nxx в сообщении #186049 писал(а):

маткиб в сообщении #186087 писал(а):

Кстати, "не может не существовать" - это значит "существует" или же это очередное конструктивистское извращение?

"Не может не существовать" - это означает, что утверждение о несуществовании опровергается, но алгоритм для построения не существует.

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

ewert в сообщении #186057 писал(а):

Есть ли утверждение о том, что любая "непрерывная" функция ограничена?

Нет. Есть теорема о том, что всякая конструктивная функция непрерывна. И есть пример конструктивной (и, стало быть, непрерывной) на $[0,1]$ функции, которая не ограничена. А равномерно непрерывная на $[0,1]$ функция хотя и ограничена, но может не достигать своего наибольшего значения.

[Nxx]

Цитата:

Странное утверждение. Откуда же тогда известно, что они не остановятся? В свете сказанного выше.

Из теоремы.

Цитата:

Не понял, причём тут теория сложности. Она что, отменяет физические ограничения на возможности физических устройств?

Она дает возможность определить, что можно решить эффективно.

[ewert]

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

Нет. Есть теорема о том, что всякая конструктивная функция непрерывна. И есть пример конструктивной (и, стало быть, непрерывной) на $[0,1]$ функции, которая не ограничена. А равномерно непрерывная на $[0,1]$ функция хотя и ограничена, но может не достигать своего наибольшего значения.

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

[маткиб]

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

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

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

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

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

Какое отношение имеет существование решателя к его описываемости каким-то там "высказыванием"?

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

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

Но в чём Вы противоречие углядели с существованием этого решателя?

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

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

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

Вы так говорите, потому что Вам это очевидно. А кому-то другому, может быть, не очевидно. Я вот, например, тоже не понимаю, чем счётное множество хуже конечного, но Вам же не очевидно? А кому-то не очевидно, что 1000 ничем не хуже, чем 100.