Уважаемый Гастрит,

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

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

2) Пи-1 платонизм - это вера (ну или "набор образов") в то, что каждая машина тьюринга или когда-то остановится или никогда не остановится. Еще Брауэра часто упрекали в том, что он математический платонист (не просто Пи-1, а вообще!!!), и многих конструктивистов с тех пор тоже. Так что я ничего нового не сказал.

3) Про Марковские взгляды и их эволюцию - тут я действительно подзабыл. Последний раз интересовался конструктивной математикой лет 10-12 назад.
Поясните пожалуйста еще раз, в чем ошибка. Я валю в одну кучу Гудстейновский рекурсивный анализ, реализуемость, книжку Клини и Уэсли, советский конструктивизм и т д.
и классифицирую их в виде спектра. Я точно помню, что в одной части спектра вещественное число было парой из двух машин тюринга (или марковских машин со скобочками): первая вычисляла последовательность рациональных чисел, а вторая - внутреннюю сходимость (в себе). По-моему это у меня в голове осталось из кннижки Кушнера.
Проблема остается: даже "в высшем смысле" вычислимая функция обычно не будет РА-доказуемо рекурсивной.

4) Правильно ли я понял, что вы находитесь в той части спектра конструктивистских философий, в которой лишь Делта_0 формулы и очень очень немногие Сигма_1 арифметические формулы будут объявлены истинными? Остальные формулы будут навсегда "зависшими".

5) Я не понял до конца Ваше отношение к доказательствам: есть замечательные формальные системы арифметики и анализа с хорошо разработанной конструктивной логикой.
В этих системах доказывается всё что нужно с помощью конструктивно приемлимых методов. В чем проблема?

(Reply to this) (Parent) (Thread)

> 2) Пи-1 платонизм - это вера (ну или "набор образов") в то,
> что каждая машина тьюринга или когда-то остановится
> или никогда не остановится.

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

> Еще Брауэра часто упрекали в том, что он математический платонист
> (не просто Пи-1, а вообще!!!), и многих конструктивистов с тех пор тоже.

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

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

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

> Проблема остается: даже "в высшем смысле" вычислимая функция обычно не будет РА-доказуемо рекурсивной.

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

> Правильно ли я понял, что вы находитесь в той части спектра
> конструктивистских философий, в которой лишь Делта_0 формулы
> и очень очень немногие Сигма_1 арифметические формулы
> будут объявлены истинными? Остальные формулы будут
> навсегда "зависшими".

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

> В этих системах доказывается всё что нужно с помощью конструктивно приемлимых методов. В чем проблема?

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

С уважением,
Гастрит

(Reply to this) (Parent)