Разговор опять перешёл в какую-то схоластическую плоскость.

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

(0) На данный момент наука не располагает никакими
результатами, которые говорят за или против следующей
возможности: наша вселенная устроена так, что в ней
можно построить лишь конечное число конструктивных объектов.
(1) Как следствие, обоснование преимущества
конструктивной математики над классической должно
оставаться верным при принятии гипотезы, указанной
в предыдущем пункте.
Подчёркиваю, что в этом пунтке я не выступаю в поддержку
или против этой гипотезы, я всего лишь говорю, что
поскольку у нас нет никаких научных доводов
против этой гипотезы, её нельзя исключать из рассмотрения.
(2) В предположении гипотезы пункта (0) существует
натуральное число, имеющее материальное представление,
такое, что если к нему добавить единицу,
то получившееся число уже не будет иметь
материального представления.
(3) Итого, в предположении гипотезы пункта (0)
имеем, что утверждение «к любому
конструктивному, уже построенному, числу можно добавить
единицу» неверно (в том смысле, что результат
не имеет материального представления).
(4) В результате, утверждение «данный алгоритм
для любых конструктивных, уже построенных, натуральных
чисел строит их сумму» следует отбросить
как бессодержательное (в смысле пункта (3)).
(5) Мы получили, что последовательное применение
материалистической точки зрении приводит к тому, что
мы вынуждены оставаться в рамках конечной математики,
в которой, например, не любые два числа можно сложить.
(А только такие, у которых сумма не очень велика.)

(Reply to this) (Parent) (Thread)

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

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

Всех благ.

(Reply to this) (Parent) (Thread)

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

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

>помните, как Вы блестяще пролетели с аксиомой бесконечности? — начинает с милой улыбкой изрекать "ну, не шмогла я", как будто ничего особенного и не случилось

Это уже исправлено. Ваш аргумент рассыпался.

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

(Reply to this) (Parent) (Thread)

Аксиомы ZF взяты из головы Цермело и немножко из головы Френкеля, т.е. они достаточно произвольны. У меня есть теория труляляшек, гораздо более правильное основание для математики.

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

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

(Reply to this) (Parent) (Thread)

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

(Reply to this) (Parent) (Thread)

>а они придуманы конкретным, никак не обоснуемым способом

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

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

(Reply to this) (Parent) (Thread)

Исходя из практики математичских рассуждений можно придумать не только ZF, но и много какие другие теории, с самыми разными результатами. Чем плохо NF?

Да с AC история известная. Книжка есть про это старинная:
В.Г.Кановей "Аксиома выбора и аксиома детерминированности". Шедевр.

Я имел в виду, что и арифметические следствия у разных теорий будут разные.

(Reply to this) (Parent) (Thread)

>Исходя из практики математичских рассуждений можно придумать не только ZF, но и много какие другие теории, с самыми разными результатами. Чем плохо NF?

Я ровно это и хотел сказать:
>Другое дело, что другие люди при том же самом
>анализе могут получить другие результаты.

>Я имел в виду, что и арифметические следствия у разных теорий будут разные.

Да, конечно, я этого не отрицаю.

(Reply to this) (Parent)

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

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

--- вероятно это так.

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

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

> (2) В предположении гипотезы пункта (0) существует натуральное число, имеющее материальное представление,
> такое, что если к нему добавить единицу, то получившееся число уже не будет иметь материального представления.

--- не в предположении пункта (0) а в предположении, что "вселенная конечна".
Я плохо понимаю, что значит "вселенная конечна" но пускай...

> (3) Итого, в предположении гипотезы пункта (0) имеем, что утверждение «к любому конструктивному, уже построенному, числу можно добавить единицу» неверно (в том смысле,
> что результат не имеет материального представления).

--- пускай... (не должно ни на что влиять).

> (4) В результате, утверждение «данный алгоритм для любых конструктивных, уже построенных, натуральных
> чисел строит их сумму» следует отбросить как бессодержательное (в смысле пункта (3)).

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

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

--- нет, такой аргумент никуда не годится.


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

Проблема с ограничением науки конструктивными рассуждениями, в том , что они не могут доказать даже некоторые простые дельта-0 формулы.
Например существование последовательности из N конечных деревьев таких что |T_i|< 5+i и предывущие деревья не вкладываются с сохранение инфимума в последующие,
легко доказывается непредикативнуми методами (выше ATR_0), то есть слегка использует понятие актуальной бесконечности, при этом даже можно с помощью этих же непредикативных методов прикинуть, где сидит это число N. Не такое уж оно и большое. В конструктивной математике вопрос о существовании такой конечной последовательности навсегда останется нерешенным (по теореме Фридмана). Это нужное и важное число. Его даже (по модулю некоторых неконструктивных теорем) можно повычислять.

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

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

(Reply to this) (Parent) (Thread)

я имел в виду максимальное 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)

>--- почему? Мы же не собираемся вдаваться в догматизм. У конструктивистов натуральные числа - деревянные палочки (например спички), а на объекты вселенной.

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

Я всего лишь хочу указать на то, что на полное
соответствие с концепцией материального воплощения
в виде объектов вселенной могу претендовать указанные
вами информатики и feasibility-believers.

Пример с деревьями замечательный. А константа 5 критична?

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

С этим я и не спорю.

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

(Reply to this) (Parent) (Thread)

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

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

Нет, я не знаю с числа 5 начинается крускальщина или может быть с числа 3, 6 или 9, но точно с какого-то маленького.

(Reply to this) (Parent)