я имел в виду максимальное N с этим свойством.

(Reply to this) (Parent) (Thread)

(spasibo---хотя я просил объяснить позицию конструктивистов, а не в каком-либо смысле защитить)

A порядок N какой --- двойная экспонента или экспонента экспонент или больше ?

И правильно ли я понимаю, что аргументы (0)-(4) говорили, что конструктивизм - нельзя обосновать внутри финитизма ?

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

Верно ли я понимаю, что точнее так : конструктивист *представляет себе* натуральное число как кучку деревянных палочек, *абстрагируясь* от физической реализуемости этой кучки*) ?

(Reply to this) (Parent) (Thread)

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

2) нет, аргументы с "конечной вселенной" не имеют отношения к философии финитизма.

3) да, представлят себе деревянные палочки (спички) и "абстрагируется", но не слишком сильно: всегда нужно не сомневаться, что то, что мы делаем с палочками можно сесть и сделать.

4) конструктивисты докомпьютерной эры (1950х-1960х годов) не интересовались вопросами сложности вычислений, поэтому сейчас их дискурс с легкостью критикуют информатики, на основании современных представлений бытующих в головах computer scientistов.

(Reply to this) (Parent) (Thread)

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

>да, представлят себе деревянные палочки (спички) и "абстрагируется", но не слишком сильно: всегда нужно не сомневаться, что то, что мы делаем с палочками можно сесть и сделать.

Вы всё опять запутали. Как понимать слова сесть и сделать?
Конкретный пример: http://en.wikipedia.org/wiki/Graham_number
Вот я сейчас сяду и напишу программу для машины Тьюринга,
которая всё в лоб перебирает, пока не найдёт правильный ответ.
Теоретически она может работать вплоть до, скажем,
примерно половины этого числа Грехема.
Такое число мы не сможем записать никогда.
Допустима ли такая программа с точки зрения конструктивизма?
Если да, то как следует понимать ваши слова про сесть и сделать?

>конструктивисты докомпьютерной эры (1950х-1960х годов) не интересовались вопросами сложности вычислений, поэтому сейчас их дискурс с легкостью критикуют информатики, на основании современных представлений бытующих в головах computer scientistов.

Это конечно. Собственно, моя критика является очень слабой
версией этой критики.

(Reply to this) (Parent) (Thread)

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

(Reply to this) (Parent) (Thread)

Очень интересно. Впрочем, это не отменяет моего вопроса
про конструктивность вычисления с числом операций порядка числа Грехема.

Было бы очень интересно узнать про эти эшелоны чуть подробнее.
Что это за Пи-1-2 анализ такой, например?
Возможно, имеет смысл написать отдельный (не очень большой) пост про это?

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

(Reply to this) (Parent) (Thread)

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

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

Про разные теории можно почитать в книжке S.Simpson "Subsystems of second-order arithmetic".

Про недоказуемость - в моей недавней писульке здесь: article

Про t(n) (и про соответствующие большие числа из диофантовыx игр) я пока серьезно не думал, хотя кое-какие банальности про доказуемо-рекурсивные функции сказать мог бы.

(Reply to this) (Parent)

А можно привести пример какого-нибудь утверждения,
верного с точки зрения конструктивной математики,
но неверного с точки зрения информатиков и feasibility-believers?

(Reply to this) (Parent) (Thread)

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

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

ПризнАют ли конструктивисты теорему Рамсея?
С конструктивистами немножко непонятно про которое крыло конструктивистской философии мы говорим.

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

Простой вопрос: почему экспонента тотальна: ответ будет такой у разных людей

у Сазонова - что экспонента не тотальна
у информатиков-физибильщиков - пожатие плечами и бормотание "а в чем вопрос?"
у конструктивистов - потому что есть тюрингова машина, которая вычисляет экспоненту.

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

Вот такой мой ответ: конструктивисты из рекурсивного анализа могут доказать больше, чем информатики-физибильщики, а эмпирические конструктивисты - меньше!

(Reply to this) (Parent) (Thread)

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

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

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

[1] О логике конструктивной математики// Вестник МГУ. Серия 1: Математика, Механика. — 1970. — Т.25, №2. — С.7-29.
[2] О логике конструктивной математики. М.: Знание, 1972.
[3] Попытка построения логики конструктивной математики// Исследования по теории алгорифмов и математической логике. — 1976. — Т.2 — С.3-31.

Вопросы, связанные с "общерекурсивностью", обсуждаются в §7 брошюры [2] и §2 статьи [3].

> В этом смысле конструктивисты являются радикальными Пи-1 платонистами

До сих пор мне не доводилось слышать, чтобы Маркова называли платонистом (его, самое большее, в "позитивисты" зачисляли). Что-то новенькое. Видимо, наиболее ярким проявлением марковского платонизма следует считать пассаж из [2, §15] про абстракцию актуальной бесконечности и аналогичные по духу издевательства над свободно становящимися последовательностями там же и в комментариях к Гейтингу.

> у конструктивистов - потому что есть тюрингова машина, которая вычисляет экспоненту.

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

> Но доказательство того, что эта машина вычисляет экспоненту
> не может быть проведено в теории слабее, чем EFA!!!

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

> пускай без принципа Маркова

С точки зрения самого Маркова, ленинградский принцип — это, вообще-то, теорема ;-) Ссылки дать?

> конструктивная математика - чисто эмпирическая наука

"Эмпирическая наука" — это сухая вода, такого не бывает. Наука устанавливает закономерности, а никакой эксперимент сам по себе никогда не докажет, что 2+2=4: он может лишь проконстатировать, что в такой-то конкретный четверг (через 10 минут 03 секунды после дождя) результат сложения 2+2, проведённый на ЭВМ с такими-то серийными номерами комплектующих, оказался равен 4. Так что по-настоящему последовательный "эмпиризм" вообще должен не теории строить, а просто протоколы экспериментов собирать: вчера насчитали то-то и то-то, год назад — то-то и то-то, а что насчитаем завтра и имеется ли какая-нибудь система в уже насчитанном — неизвестно (и даже думать на эту тему низ-зя, патамушта схоластика!)

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

(Reply to this) (Parent) (Thread)

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

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)