>Или ВЧ — это фундаментальная последовательность рациональных чисел? Но где эта последовательность в Вашем случае — я у Вас тут только несколько буковок вижу.

Пожалуйста, берёте частичную сумму ряда, вот вам фундаментальная последовательность.

>Пока этого не произошло, физикам плевать на математическую некорректность своих выкладок. Т.е. действительное отношение физиков к математике таково: когда математики "разрешают" делать нечто желаемое физикам, то последние на соответствующие теоремы с удовольствием ссылаются; когда же математики желаемое, напротив, "запрещают", то физики попросту делают вид, что такого запрета не существует.

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

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

(1) В настоящее время физики активно используют классическую
математику (теорема Лефшеца, К-теория, спектральная последовательность Атии-Хирцебруха).
Ваши указания на нестрогость физики здесь не помогают —
путём наблюдений за историей установлено, что
все нестрогие результаты рано или поздно превращаются
в строгие.
(2) Классическая математика работает в физике.
То есть физики предсказывают с её помощью физические
явления, после чего ставят эксперимент и обнаруживают,
что его результаты совпадают с теоретическим предсказаниями.
При этом в физике используются теоремы, конструктивные
аналоги которых попросту неверны (теорема Лефшеца).
(3) Что касается конструктивной математики, то пока
никто не продемонстрировал, каким образом конструктивная
математика позволяет предсказывать физические
явления лучше, чем классические. Это и не удивительно,
если учесть, что всё, что доказуемо в конструктивной
математике, доказуемо и в классической, а вот некоторые
результаты классической, вроде теоремы Лефшеца, неверны
в конструктивной.
(4) Наука о программировании и связанных с ним
закономерностях — это не математика, а computer science,
которая далеко не исчерпывает математику.
Это общепринятое определение и не надо
пытаться подгонять определение математики под свои взгляды.

>Уже давал (про "единственный способ — приложение к физике").
Это про другое.

>Тогда какая из конкурирующих аксиоматик теории множеств объективно верна? почему верна именно она? где можно посмотреть на её модель?

В математике нет абсолютных утверждений.
Как я уже указывал, хотя может показаться обратное,
по сути все утверждения в математике имеют вид:
Если T — вполне отделимый элементарный топос с объектом натуральных чисел, то тогда верно X. (Это ZF.)
Если T — вполне отделимый элементарный топос с объектом натуральных чисел, в котором выполнена аксиома выбора, то тогда верно X. (Это ZFC.)
Если T — эффективный топос, то тогда верно X. (Это конструктивная математика.)
Такие утверждения объективны верны в любом разумном
смысле этого слова.

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

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

(Reply to this) (Parent) (Thread)

> Пожалуйста, берёте частичную сумму ряда, вот вам фундаментальная последовательность.

Простите великодушно, а это не в Вашей "классической" математике последовательность определялась как «всюду определённая функция натурального аргумента»? Давно ли частичная сумма у нас превратилась из числа в функцию?

> А если математики предлагают способ устранить неформальные
> выкладки, то физики его используют.
> Физики пользуются нестрогими рассуждениями не потому,
> что им так хочется, а потому, что у них нет другого выхода.

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

> (1) В настоящее время физики активно используют классическую
> математику (теорема Лефшеца, К-теория, спектральная последовательность Атии-Хирцебруха).

Не потому, что им так хочется, а потому, что у них нет другого выхода — Ваши же слова. А Вы ещё и хотите им этот выход заколотить на веки вечные, хотя Ваша прямая обязанность как математика состоит прямо в обратном. Милое дело!

> При этом в физике используются теоремы, конструктивные
> аналоги которых попросту неверны (теорема Лефшеца).

Не потому, что физикам так хочется, а потому, что у них нет другого выхода.

> (3) Что касается конструктивной математики, то пока
> никто не продемонстрировал, каким образом конструктивная
> математика позволяет предсказывать физические
> явления лучше, чем классические.

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

> Это и не удивительно,
> если учесть, что всё, что доказуемо в конструктивной
> математике, доказуемо и в классической, а вот некоторые
> результаты классической, вроде теоремы Лефшеца, неверны
> в конструктивной.

А в "наивной" теории множеств Кантора доказуемо вообще всё (ввиду её противоречивости). Давайте уж сразу на неё перейдём, а?

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

Поток сознания. Вы хоть точную формулировку-то теоремы Гёделя знаете?

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

(Reply to this) (Parent) (Thread)

>Простите великодушно, а это не в Вашей "классической" математике последовательность определялась как «всюду определённая функция натурального аргумента»? Давно ли частичная сумма у нас превратилась из числа в функцию?

Частичная сумма первых k членов ряда образует
всюду определённую функцию натурального аргумента, которая
является фундаментальной последовательностью.

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

Не очень понимаю что вы имеете в виду под «канонизацией».
Что касается теоремы Лефшеца, то, как я уже говорил,
она верна в классическом случае, но неверна в конструктивном.
Если вы ведёте беседе в узком кругу конструктивистов,
вы можете подразумевать конструктивный случай,
однако в общематематической дискуссии извольте добавлять
словосочетание «в конструктивной математике».

Я, как видите, эти два случая различаю.

>Не потому, что им так хочется, а потому, что у них нет другого выхода — Ваши же слова.

Это не соответствует действительности.
Если бы физикам были доступны строгие средства,
они бы их использовали.
Если бы физикам были доступны конструктивные средства,
они бы их проигнорировали. Уже хотя бы потому,
что классическая математика (созданная при участии
физики) для нужд физики адекватнее.

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

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

>А в "наивной" теории множеств Кантора доказуемо вообще всё (ввиду её противоречивости). Давайте уж сразу на неё перейдём, а?

Теория Кантора неформальна.
Противоречивы некоторые формализации теории Кантора,
которые предложили другие люди (не Кантор).
У вас есть что возразить по существу дела?

>Поток сознания. Вы хоть точную формулировку-то теоремы Гёделя знаете?

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

(Reply to this) (Parent) (Thread)

> Частичная сумма первых k членов ряда образует
> всюду определённую функцию натурального аргумента, которая
> является фундаментальной последовательностью.

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

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

Научная математика — это и есть конструктивная математика. Честные "классики" сие и сами прекрасно знают, а потому сразу говорят, что математика для них — не наука. К таким у меня вопросов нет, такие о "верности" своих теорем не рассуждают (как можно ставить вопрос о "верности" героической симфонии Бетховена? или «Адама» Микеланджело?). А вот которые рассуждают, к тем сразу вопрос: верными утверждениями о чём являются Ваши теоремы?

Теперь о неподвижных точках. Как уже говорилось, любое измерение проводится с отличной от нуля точностью. Поэтому для физика неподвижной будет и такая точка, которая на деле вполне себе подвижна, но уходит от изначального положения "не очень далеко". Задача математиков тут — изучить вопрос о наличии таких точек (в зависимости от свойств отображения, величины "точности неподвижности", и т.д.). А что они делают вместо этого? Гордо предъявляют заведомо неверную (но столь же заведомо могущую стать верной при внесении некоторых корректив в формулировку, искать каковые коррективы математики попросту не хотят, хотя это — их профессиональная обязанность) теорему и заваливаются на печку. Простите, но это (т.е. рассуждать на пальцах в надежде, что авось прокатит) физики и сами умеют!

> Если бы физикам были доступны строгие средства,
> они бы их использовали.
> Если бы физикам были доступны конструктивные средства,
> они бы их проигнорировали.

А Вы не решайте за физиков. Считать коллег идиотами, не способными разобраться, что им нужно — не лучший способ аргументации (Ваши слова, не так ли?). Вот тот же Ландау утверждал, что преподавать физикам "классическую" математику — это спасать их души вопреки их желанию; что им (физикам) "классическая" математика нужна не более, чем средневековая схоластика. Что, Ландау, по-Вашему, не физик был?

> Давайте условимся: если я использую в своей аргументации
> какой-то объект, то я знаю его определение.
> У вас есть что возразить по существу дела?

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

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

(Reply to this) (Parent) (Thread)

>Садитесь, "два". Причём именно по "классической" математике (в которой функция — это множество упорядоченных пар, такое, что бла-бла-бла). Где здесь функция в том смысле, в котором этот термин определяется в ZF, а не в учебниках высшей математики для заборостроительных вузов?

Это множество пар вида (k, s_k), где s_k —
сумма первых k членов ряда.

>А вот которые рассуждают, к тем сразу вопрос: верными утверждениями о чём являются Ваши теоремы?

Ваши теоремы являются верными утверждениями об
объектах воображаемой вселенной, в которой
существуют машины с неограниченным объёмом памяти.
Мои теоремы являются верными утверждениями об
объектах воображаемой вселенной, в которой
существуют машины, действующие по правилам ZF.

>Теперь о неподвижных точках. Как уже говорилось, любое измерение проводится с отличной от нуля точностью. Поэтому для физика неподвижной будет и такая точка, которая на деле вполне себе подвижна, но уходит от изначального положения "не очень далеко". Задача математиков тут — изучить вопрос о наличии таких точек (в зависимости от свойств отображения, величины "точности неподвижности", и т.д.). А что они делают вместо этого? Гордо предъявляют заведомо неверную (но столь же заведомо могущую стать верной при внесении некоторых корректив в формулировку, искать каковые коррективы математики попросту не хотят, хотя это — их профессиональная обязанность) теорему и заваливаются на печку. Простите, но это (т.е. рассуждать на пальцах в надежде, что авось прокатит) физики и сами умеют!

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

>А Вы не решайте за физиков. Считать коллег идиотами, не способными разобраться, что им нужно — не лучший способ аргументации (Ваши слова, не так ли?). Вот тот же Ландау утверждал, что преподавать физикам "классическую" математику — это спасать их души вопреки их желанию; что им (физикам) "классическая" математика нужна не более, чем средневековая схоластика. Что, Ландау, по-Вашему, не физик был?

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

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

В сочетании с тезисом о формализуемости математических
доказательств в формальных системах мы как раз и получаем то, что хотели.

(Reply to this) (Parent) (Thread)

> Это множество пар вида (k, s_k), где s_k —
> сумма первых k членов ряда.

Слова, слова, слова. Я Вам конструктивное вещественное число приводил? Приводил. Теперь Вы приведите неконструктивное. Не почёрпнутое из учебников для заборостроительного института описание этого числа (которое Вы пока пытаетесь мне всучить), а само число. До этого момента обсуждать нечего.

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

Мои теоремы являются утверждениями о реальной вселенной.

> Мои теоремы являются верными утверждениями об
> объектах воображаемой вселенной, в которой
> существуют машины, действующие по правилам ZF.

Вот поэтому-то Ваши теоремы (в отличие от моих) и ненаучны.

> Видите ли, всё уже давно изученно.

С ошибками изучено. И Вы эти ошибки исправлять не хотите. Что ж, хозяин барин.

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

Какая у Ландау была "считательная математика", я уже цитаты приводил. Она не "классическая", она XVIII века: с актуальными бесконечно малыми и очевидностью возможности перехода к пределу для всего подряд. Выкинуть же он предлагал именно Вашу "классическую".

> В сочетании с тезисом о формализуемости математических
> доказательств в формальных системах мы как раз и получаем то, что хотели.

Этот тезис является бредовым. Продолжайте.

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

(Reply to this) (Parent) (Thread)

>Слова, слова, слова. Я Вам конструктивное вещественное число приводил? Приводил. Теперь Вы приведите неконструктивное. Не почёрпнутое из учебников для заборостроительного института описание этого числа (которое Вы пока пытаетесь мне всучить), а само число. До этого момента обсуждать нечего.

А что я, по-вашему, делаю? Я уже построил
в явном виде это неконструктивное число. Не его описание,
а само это число. Фундаментальную последовательность
рациональных чисел.

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

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

>С ошибками изучено. И Вы эти ошибки исправлять не хотите. Что ж, хозяин барин.

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

>Какая у Ландау была "считательная математика", я уже цитаты приводил. Она не "классическая", она XVIII века: с актуальными бесконечно малыми и очевидностью возможности перехода к пределу для всего подряд. Выкинуть же он предлагал именно Вашу "классическую".

Пожалуйста, дайте точную ссылку на Ландау, где
он предлагает выкинуть классическую математику
и оставить 18 век.
До тех пор все эти слова являются спекуляцией.
Могу добавить, что вычисление какой-либо
физической величины с помощью теоремы Лефшеца
— это считательная математика по Ландау.

>Этот тезис является бредовым. Продолжайте.

Что ж, не потрудитесь ли привести пример
доказательства, неформализуемого в формальной системе?
За слова надо отвечать.

Я полагаю, что вы знаете, что вся конструктивная
математика держится на тезисе Чёрча.
Что если я объявлю этот тезис бредовым?

(Reply to this) (Parent) (Thread)

> А что я, по-вашему, делаю? Я уже построил
> в явном виде это неконструктивное число. Не его описание,
> а само это число. Фундаментальную последовательность
> рациональных чисел.

Ничего Вы не построили, только руками намахали. Соответственно, обсуждать нечего.

> Вы же утверждаете, что все натуральные числа являются
> конструктивными объектами, а их бесконечное число.

Ссылочку дайте, где я употреблял слово "все" применительно к натуральным числам. Самим-то постоянно передёргивать не надоело?

> Их научность совпадает с научностью ваших
> теорем

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

> вы предполагаете существование некой
> вселенной с бесконечным количеством материи,

Этот бред Вы можете ещё хоть тысячу раз повторить; более верным он от этого не станет.

> У вас есть что возразить по существу?

По данному пункту я давно всё сказал, причём не по одному разу. Если же у Вас трудности с чтением — тут я, увы, бессилен :-(

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

(Reply to this) (Parent)

Я понял!!! dmitri_pavlov@lj — бот! То-то я удивлялся, с чего это он по сто раз повторяет одни и те же вопросы (и полностью игнорирует ответы) — ну, а как же ему иначе-то: что в базу запузырили, то он и штампует. Слава роботам! Крутая машинка получилась!

Ну вот, к примеру:

> Пожалуйста, дайте точную ссылку на Ландау, где
> он предлагает выкинуть классическую математику
> и оставить 18 век.

Не так давно пробегала цитата из «Квантовой электродинамики», где упоминались "бесконечно малые интервалы" (взятые непосредственно у Лейбница) и много чего ещё в том же роде. Человек бы эту цитату прочитал и оценил. Но бот, понятное дело, этого провернуть не в состоянии, вот и бегает по кругу.

> Могу добавить, что вычисление какой-либо
> физической величины с помощью теоремы Лефшеца
> — это считательная математика по Ландау

У человека я бы попросил привести ссылки на использование Ландау этой теоремы или других теорем чистого существования (которые сам же он и костерил последними словами), но с бота какой же спрос :-)

> Что ж, не потрудитесь ли привести пример
> доказательства, неформализуемого в формальной системе?
> За слова надо отвечать.

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

> Я полагаю, что вы знаете, что вся конструктивная
> математика держится на тезисе Чёрча.
> Что если я объявлю этот тезис бредовым?

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

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

(Reply to this) (Parent) (Thread)

Я просил бы Вас более уважительно отзываться о собеседнике.


> Пожалуйста, дайте точную ссылку на Ландау, где
> он предлагает выкинуть классическую математику
> и оставить 18 век.

Вас просили дать _точную ссылку_. Точной ссылки, кажется, не было...

> Что ж, не потрудитесь ли привести пример
> доказательства, неформализуемого в формальной системе?
> За слова надо отвечать.

Доказательство непротиворечивости самой этой формальной системы (в случае, если она действительно непротиворечива).

действительно, любопытное замечание.


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

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

(Reply to this) (Parent) (Thread)

> Я просил бы Вас более уважительно отзываться о собеседнике.

Я бы с удовольствием. Но после получения сотни постов в стиле "а ты всё-таки купи слона"...

> Вас просили дать _точную ссылку_. Точной ссылки, кажется, не было...

Было упоминание известного (в том числе и моему оппоненту, судя по его замечаниям) письма Ландау со словами «я категорически считаю, что из математики, изучаемой физиками, должны быть полностью изгнаны всякие теоремы существования, слишком строгие доказательства и т.д.», «необходимость в курсе теории вероятностей довольно сомнительна, физики и без того излагают то, что им нужно, в курсах квантовой механики и статистической физики» (курсив мой). И были приведены конкретные (там даже номер параграфа из ссылок легко вытаскивается) указания на то, что же именно физики "и без того излагают". Sapienti sat.

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

Способы построения этих алгорифмов очень даже выписывают. В той же «Теории алгорифмов» Маркова (или более позднем варианте Маркова-Нагорного) явные доказательства теорем о сочетании занимают чуть не полкниги. Ссылка на тезис Чёрча в качестве элемента доказательства в конструктивной математике не допускается.

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

(Reply to this) (Parent) (Thread)

>Было упоминание известного (в том числе и моему оппоненту, судя по его замечаниям) письма Ландау со словами «я категорически считаю, что из математики, изучаемой физиками, должны быть полностью изгнаны всякие теоремы существования, слишком строгие доказательства и т.д.», «необходимость в курсе теории вероятностей довольно сомнительна, физики и без того излагают то, что им нужно, в курсах квантовой механики и статистической физики» (курсив мой). И были приведены конкретные (там даже номер параграфа из ссылок легко вытаскивается) указания на то, что же именно физики "и без того излагают". Sapienti sat.

Как раз эта цитата мне хорошо известна, и того, что вы приписываете Ландау (вернуться в 18 век) в ней нет.

>должны быть полностью изгнаны всякие теоремы существования
Теорема Лефшеца не является теоремой существования,
это — вычислительный инструмент. Которым
физики с удовольствием пользуются.

(Reply to this) (Parent)

>Я понял!!! dmitri_pavlov — бот! То-то я удивлялся, с чего это он по сто раз повторяет одни и те же вопросы (и полностью игнорирует ответы) — ну, а как же ему иначе-то: что в базу запузырили, то он и штампует. Слава роботам! Крутая машинка получилась!

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

>Не так давно пробегала цитата из «Квантовой электродинамики», где упоминались "бесконечно малые интервалы" (взятые непосредственно у Лейбница) и много чего ещё в том же роде. Человек бы эту цитату прочитал и оценил. Но бот, понятное дело, этого провернуть не в состоянии, вот и бегает по кругу.

Эта цитата никакого отношения к делу не имеет.
То, что человек использует бесконечно малые, не означает,
что он предлагает вернуться к математики 18 века.

>У человека я бы попросил привести ссылки на использование Ландау этой теоремы или других теорем чистого существования (которые сам же он и костерил последними словами), но с бота какой же спрос :-)

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

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

Вы умеете доказывать непротиворечивость формальных систем с арифметикой?
Уже подали заявку на филдсовскую медаль?

>Объявляйте сколько угодно, конструктивная математика от этого не пострадает.

В таком случае, вы, видимо, не знаете, что такое тезис Чёрча.

(Reply to this) (Parent) (Thread)

За Вашей дискуссией мне не уследить, но это место мог бы прокомментировать.

Вы умеете доказывать непротиворечивость формальных систем с арифметикой? Уже подали заявку на филдсовскую медаль?

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

Но, вообще говоря, здесь вероятно
имеется в виду тривиальное доказательство --- формальная система непротиворечива если имеет модель. Арифметика Пеано модель имеет, как легко видеть. Также легко видеть, что и теория множеств имеет модель--ну может несколько сложнее.)

(Reply to this) (Parent) (Thread)

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

Это доказательство Генцена, если я всё правильно
понимаю. Сама теорема, конечно, замечательная.
Правда есть лёгкая проблема: доказательство
непротиворечивости проводится в более сильной системе.
Возникает вопрос: а как насчёт непротиворечивости
этой более сильной системы? И так далее.

(Reply to this) (Parent) (Thread)

Я не совсем понимаю, что мы обсуждаем. Из доказательство Генцена
действительно следует, что в арифметике Пеано не вывести вполнеупорядоченность этого кардинала.

Но мне показалось, что Вы сказали, что непротиворечивость арифметики Пеано нельзя доказать неформально--видимо, я неправильно Вас понял---и привел такое доказательство (она имеет модель).


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

(Reply to this) (Parent) (Thread)

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

Теорема Генцена — это обычная теорема классической
математики. Она прекрасно формализуется (в примитивно
рекурсивной арифметике с индукцией до эпсилон-нуль
для формул без кванторов)
и доказывает непротиворечивость арифметики с логикой
первого порядка. Естественно, что это доказательство
соответствует любым стандартам строгости математики,
более того, оно вполне формально.

Единственное, что я неправильно сказал, что эта
формальная система сильнее обычной арифметики —
они просто не сравнимы.

Я сейчас посмотрел Википедию по этому вопросу и обнаружил,
что ничего не напутал:

In 1936 Gerhard Gentzen proved the consistency of first-order arithmetic using combinatorial methods. In itself, the result is rather trivial, since the consistency of first-order arithmetic has a very easy proof: the axioms are true—in a mathematically defined sense—the rules of predicate calculus preserve truth and no contradiction is true, hence no contradiction follows from the axioms of first-order arithmetic. What makes Gentzen's proof interesting is that it shows much more than merely that first-order arithmetic is consistent. Gentzen showed that the consistency of first-order arithmetic is provable, over the weaker base theory of primitive recursive arithmetic with the additional principle of quantifier free transfinite induction up to the ordinal ε0 (epsilon nought).

То есть речь в данном случае идёт скорее не о неформальном
доказательстве (доказательство теоремы Генцена
вполне формально), а о какой-то неформальной интерпретации этого
доказательства.

Именно эта неформальная интерпретации нас и интересует.
Не могли бы вы дать какие-то ссылки на описание
этой неформальной интерпретации?
Просто что вижу я — это что теорема Генцена
сводит вопрос о непротиворечивости формальной
системы с арифметикой и логикой первого порядка
к непротиворечивости другой (несравнимой с ней)
формальной системы.

(Reply to this) (Parent) (Thread)

Именно эта неформальная интерпретации нас и интересует.
Не могли бы вы дать какие-то ссылки на описание
этой неформальной интерпретации?

Я не совсем понимаю вопрос, стандартная ссылка -- Такеути,
Takeuti, Proof theory (2nd edition is better), Введение.

Философский смысл доказательства Генцена
примерно такой; нас интересует, насколько и в какой форме
понятие "актуальной бесконечности" требуется для обоснования арифметики.
Поэтому мы хотим доказательство непротиворечивости арифметики, скажем Пеано,
использующее "актуальной бесконечности" в наимболее слабой и наиболее явной
форме.

Доказательство Генцена является именно таким: Тheory of primitive recursive arithmetic имеет весьма ограниченный принцип индукции: для формул -- только по бескванторным формулам, для построения функций -- примитивная рекурсия

the function h defined by
h(0,x1,...,xk) = f(x1,...,xk) and
h(n+1,x1,...,xk) = g(h(n,x1,...,xk),n,x1,...,xk) is primitive recursive
if g,h are.

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

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


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

(Reply to this) (Parent) (Thread)

> Философский смысл доказательства Генцена
> примерно такой; нас интересует, насколько и в какой форме
> понятие "актуальной бесконечности" требуется для обоснования арифметики.

?! И где же в генценовских ординалах (кои суть конструктивные объекты, с вполне "конечными" операциями над ними) содержится актуальная бесконечность?

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

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

> Без сомнения, в какой-то форме используется (при абсрагировании от конструктивных особенностей)

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

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

(Reply to this) (Parent) (Thread)

?! И где же в генценовских ординалах (кои суть конструктивные объекты, с вполне "конечными" операциями над ними) содержится актуальная бесконечность?

Она нужна для обоснования трансфинитной индукции и, вообще говоря, даже индукции по формулам с кванторами.

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

там ее как роаз и нет

> Без сомнения, в какой-то форме используется (при абсрагировании от конструктивных особенностей)

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


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

(Reply to this) (Parent)

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

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

2) Дискуссия была "в стиле ретро" (~1956-1963), т.к. современные аргументы (например обратная математика) не использовались.

3) Про то, есть ли "актуальная бесконечность" в утверждении про трансфинитную индукцию до эпсилон_0 - я согласен с __gastrit, и тоже не вижу здесь актуальную бесконечность.

Обычно актуальную бесконечность подразумевают в уже непредикативных системах, выше ATR_0, или в других системах где явным образом выписано (forall X) (exists Y), где кванторы бегают "по множествам". Т.е. в системах, где явно постулируется существование законченной "актуальной" бесконечности.

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

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

(Reply to this) (Parent) (Thread)

Cпасибо за приход.


3) А как *доказать* трансфинитную индукцию без использования актуальной бесконечности?
сформулировать мы можем, да, без.. И правильно ли я понимаю, что индукция по формулам с кванторами -- не"актуальная" бесконечность? А какая?

(Reply to this) (Parent) (Thread)

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

Например примитивно рекурсивные бесконечные множества - это просто пустышки набитые точками. Их "существование" или "несуществование" - это вопрос удобства записи. Философия, признающая такие множества называется финитизм.

АCА_0, арифметика пеано определяет все арифметические множества. Здесь из любого множества можно выделять подможества с помощю формул первого порядка с кванторами и использовать индукцию. Математика с ТАКИМИ бесконечными множествами называется конечной математикой.

Дальше идут АCA^'_0, АТR_0, Pi_1^2 CA_0 и Z_2.
До АТR_0 бесконечность еще не называют актуальной, потому что нет сильных формул выделения.

На твой вопрос как обоснуется ТR(эпсилон_0) - ответ такой: доказывается в АCA^'_0, например следует из бесконечной теоремы Рамсея или из трансфинитной индукции до ординала эпсилон_{эпсилон_0}.

(Reply to this) (Parent) (Thread)

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

(Reply to this) (Parent) (Thread)

ACA^'_0 nu ili 1-neprotivorechivost' PA ne
soderzhat ssylok na aktualnuju beskonechnost' i
dokazyvajut TR(epsilon_0).

(Reply to this) (Parent)

> Дискуссия была "в стиле ретро" (~1956-1963), т.к. современные аргументы (например обратная математика) не использовались.

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

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

Основной вопрос, который тут волнует лично меня — наличие семантики. Для первопорядковой арифметики она определена (башня Маркова), и потому тут добавлять новые утверждения мы можем хоть прямо наугад: в крайнем случае, ошибку потом можно будет найти и исправить. А где семантика у формул с множественными переменными?

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

(Reply to this) (Parent) (Thread)

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

--- Спор за последние два-три поколения изменился и трансформировался. Его костяк может и похож на старый, но сейчас новое понимание.
Прогресс у человечества идет вперед. И история конструктивной математики и неконскруктивной тоже (но связанной) тоже идет вперед.
Когда-то был только Кронекер, а потом Пуанкаре, потом Брауэр, Хейтинг, Марков, Шанин. Неужели с 1960х годов мы не стали понимать больше?
Стали и очень много! Несколько революций в математической логике с 1960х годов совершенно всё изменили.
(Разница между 2000-ми годами и 1960-ми примерно такая же как между 1960-му и серединой ХиХ века.)

Я примерно на эту тему недавно даже книжку заказал в магазине, под названием "Крейзелиана".

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

--- Нет в наше время одной "теоретико-множественной" парадигмы, да и нескольких нет. Всё сложнее. Z_2 - это теория множеств или нет? Или АТR_0 или АCА_0?
как насчет интуиционистской теории множеств Микаэла Ратьена?
Да и конструктивизмов разных дюжина. Который чьему сердцу ближе?

> Поэтому сия деятельность, честно говоря, не
> представляется мне особо интересной (если я неправ, то с интересом выслушал бы, почему).

--- В логике творятся чудеса, по всему спектру филосовских фонов. Поинтересуйтесь! Очень интересно!

> Основной вопрос, который тут волнует лично меня — наличие семантики. Для первопорядковой арифметики она определена (башня Маркова), и потому
> тут добавлять новые утверждения мы можем хоть прямо наугад: в крайнем случае, ошибку потом можно будет найти и исправить.

--- Я имел в виду классическую логику. Кстати, про конструктивную арифметику: как насчет семантики Шанина?

> А где семантика у формул с множественными переменными?

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

(Reply to this) (Parent) (Thread)

Я примерно на эту тему недавно даже книжку заказал в магазине, под названием "Крейзелиана".

Дай пожалуйста ссылку на какой-нибудь обзор. А слово топос
в этой науке произносится ?

(Reply to this) (Parent) (Thread)

> Дай пожалуйста ссылку на какой-нибудь обзор.

---- Миша, на обзор чего? Логики?

> А слово топос в этой науке произносится ?

---- В которой науке??? В логике???

.

.

.

Помню, Миша, у нас с тобой был разговор зимой 1995/1996 года на лестнице в Ломи.
Я тогда, начитавшийся про конструктивную математику, интуиционизм и топосы (гольдблаттову книжку) тебе про это рассказывал страстно.
Ты послушал-послушал, покачал головой и сказал: "Это всё не интересно. Меня интересует только Сложность [вычислений]".

(Reply to this) (Parent) (Thread)

Дальше идут АCA^'_0, АТR_0, Pi_1^2 CA_0 и Z_2.
До АТR_0 бесконечность еще не называют актуальной, потому что нет сильных формул выделения.

обзор и топос в науке про эти системы и особенно бесконечности..

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

(Reply to this) (Parent) (Thread)

Misha, okroj pozhalusta novuju, otdelnuju temu pro eto. Ja chto-nibud' esche umnoe skazhu.

Pro eti sistemy - pochti vse logicheskie knizhki v mire. V Kleene oni vypisany v jazyke p[ervogo porjadka
i nazyvajutsya

RCA_0 --- primitivno rekursivnaja arifmetika

ACA_o --- arifmetika Peano

ACA^'_0 --- arifmetika Peano rasshirennaja mnogochislennymi dobavlenijami principa refleksii (rovno epsilon_{epsilon_0} raz.

(Reply to this) (Parent)

sovsem novuju temu (novyj post).

(Reply to this) (Parent) (Thread)

mozhno. no luchshe by ego sdelat' citatoj ili naborom citat
(wse eti spory uzhe sporeny-peresporeny..) any ideas ?

(Reply to this) (Parent) (Thread)

ne znaju dazhe chto i posovetovat'... Ty v kakoj sejchas strane (kotoraja biblioteka pod rukoj)?

Ja dumal chto raz u tebja PhD po logike, to ty vsyo eto ne xuzhe menja znaesh'?

Mozhno simpsonovu knizhku pochitat' konechno, no tam ne vsyo.

(Reply to this) (Parent)

> --- Спор за последние два-три поколения изменился и трансформировался.
> Его костяк может и похож на старый, но сейчас новое понимание.

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

> Неужели с 1960х годов мы не стали понимать больше? Стали и очень много!
> Несколько революций в математической логике с 1960х годов совершенно всё изменили.

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

> --- Нет в наше время одной "теоретико-множественной" парадигмы, да и нескольких нет.
> Всё сложнее. Z_2 - это теория множеств или нет? Или АТR_0 или АCА_0?

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

> Да и конструктивизмов разных дюжина. Который чьему сердцу ближе?

Дюжина не конструктивизмов; дюжина направлений, называющих себя конструктивными. Из них некоторые конструктивизмами не являются вообще (ну, какой конструктивист из того же Бишопа, у которого «нет позиции»? или из Мартин-Лёфа с его расплывчатыми ординалами?), а некоторые представляют собой механическое ковыряние в примитивно-рекурсивной арифметике (тот же Гудстейн). Чтобы где-либо формулировалась материалистическая конструктивная установка, принципиально отличная от марковской, мне неизвестно.

> --- В логике творятся чудеса, по всему спектру филосовских фонов. Поинтересуйтесь! Очень интересно!

Дайте ссылки, поинтересуюсь. Если там действительно не будет идеальных тоже-"объектов".

> --- Я имел в виду классическую логику.

Если ограничиться нормальными формулами (или механически навешивать на всё два отрицания, что то же самое), то классическая и будет.

> Кстати, про конструктивную арифметику: как насчет семантики Шанина?

Это пресловутые мажоранты, что ли? Пробовал как-то я сквозь них продраться, и мне это не особо удалось :-( Остаётся ощущение какой-то искусственности, намерения "придумать" семантику из головы, а не вывести её из давно выработанных способов рассуждений (как это делает Марков).

> --- В этом смысле и для формул первого порядка нет фиксированной семантики

С моей точки зрения, нефиксированной является всё же не сама семантика, а ответы на вопросы о верности той или иной конкретной формулы в рамках этой семантики. Хотя что это интересно, не спорю.

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

(Reply to this) (Parent) (Thread)

> С моей точки зрения, нефиксированной является всё же не сама семантика, а ответы на вопросы о верности

> той или иной конкретной формулы в рамках этой семантики. Хотя что это интересно, не спорю.

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

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

(Reply to this) (Parent) (Thread)

> Разные "семантики" возникают на разных ветках (добавлять и добавлять непротиворечивые утверждения)

Разве что именно "семантики". Меня как-то больше интересует семантика без кавычек (с вопросом о непротиворечивых расширениях исчислений не связанная).

> Есть основания математики, где математики "ищут правду",

Угу. ИМХО, именно это и называется наукой.

> некоторые - где "ищут красоту",

ИМХО, это называется искусством.

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

ИМХО, это называется профанацией.

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

ИМХО, это называется безграмотностью.

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

> И многие из них непротиворечивы.

«Неверная теория, не натолкнувшаяся на противоречие, столь же не становится от этого верной, как преступление, не наказанное правосудием, не превращается от этого в добродетель» (Брауэр). «Вопрос о непротиворечивости для конструктивиста не стоит» (Марков). А я что — я согласен :-)

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

(Reply to this) (Parent) (Thread)

ja imel v vidu neprotivorechivost' v vysshem smysle: razumnost' i obosnovannost'.

Sovremennyj pljuralizm baziruetsya ne na nevezhestve, a na tom, chto est' neskol'ko tipov mozga, neskol'ko tipov rassuzhdenij, neskol'ko tipov ponimanija, chto takoe matematika.

Esche igraet rol' nedavnjaja nauchnaja revoljutsija v evrope: um evropejtsa podelen mezhdu temnymi vekami (s traditsiej pochitanija avtoriteta, ne znaju dazhe nazyvat' li etix ljudej sxolastami) i Prosvescheniem.

Bez kavychek ne ponimaju: kakie arifmeticheskie utverzhdenija schitat' za pravdu bez kavychek? Mnogo let starajus': poka ne ponjal.

(Reply to this) (Parent) (Thread)

> Sovremennyj pljuralizm baziruetsya ne na nevezhestve,
> a na tom, chto est' neskol'ko tipov mozga,
> neskol'ko tipov rassuzhdenij,
> neskol'ko tipov ponimanija, chto takoe matematika.

2+2=4. Последовательность частичных сумм ряда \(\sum_{n=0}^{\infty} 1/n!\) фундаментальна (с эффективным регулятором). Я не знаю, какой нужно иметь тип мозга, чтобы сделать эти факты неверными (по крайней мере, в рамках доступной нам сегодня практики). Сколько не пытался запускать программу, последовательно вычисляющую вышеуказанные частичные суммы и выдающую результаты на печать — у меня никогда до 3 не доходило. Хотя, может, у буддийских бхикшу действительно всё иначе.

> Esche igraet rol' nedavnjaja nauchnaja revoljutsija v evrope:
> um evropejtsa podelen mezhdu temnymi vekami (s traditsiej
> pochitanija avtoriteta, ne znaju dazhe nazyvat' li etix ljudej
> sxolastami) i Prosvescheniem.

А у европейских ЭВМ тоже процессоры поделены таким же образом? И в одно время 7*8 у них =56, а в другое =89? Действительно, очень интересно. Я не знал.

> Bez kavychek ne ponimaju: kakie arifmeticheskie utverzhdenija schitat' za pravdu bez kavychek?
> Mnogo let starajus': poka ne ponjal

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

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

(Reply to this) (Parent) (Thread)

ja imel v vidy formuly s kvantorami.

(Reply to this) (Parent) (Thread)

Кванторами общности, то бишь (т.к. одни существования полуразрешимости не умаляют)? Ну, тамошнюю ситуацию я тоже охарактеризовал: принцип действия у нас чёткий — \(\forall xA\) означает, что при любом выборе натурального числа \(n\) результат подстановки \([A]^x_n\) будет верной формулой — проблемы могут быть только с применением этого правила к конкретным случаям.

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

(Reply to this) (Parent) (Thread)

ne ponimaju, v kakom smysle "pri ljubom vybore naturalnogo chisla"?
tak mozhno tseluju vechnost' prozhdat' (poka naturalnye chisla ne konchatsya)!!!!!

Ja tolko pro Delta_0-formuly ponimaju, a pro vse ostalnye ne ochen'.

Ja podozrevaju, chto ja konstruktivist. :)))

(Reply to this) (Parent) (Thread)

> tak mozhno tseluju vechnost' prozhdat' (poka naturalnye chisla ne konchatsya)!!!!!

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

В физике у всех общих законов ровно такая же судьба.

> Ja podozrevaju, chto ja konstruktivist. :)))

Вы, похоже, клятый финитарист, то бишь еретик и отступник :-))

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

(Reply to this) (Parent) (Thread)

v obschem ja soglasen, tak i est'... no uzh ochen' mnogo nejasnostej...

Da, i finitist tozhe. (Finitizm u menja po vtornikam.)

(Reply to this) (Parent)

i kak naschet neskolkix kvantorov?

(Reply to this) (Parent) (Thread)

Индукция по логической длине рулит :)

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

(Reply to this) (Parent) (Thread)

net, ne poluchaetsya po induktsii. kvantory cheredujutsya.

Kak ponjat' pravda ili net Pi-2 formula (forall x)(exists y) phi(x,y)
esli uzhe pri x=1 slishkom dolgo zhdat' i ne dozhdat'sja?

(Reply to this) (Parent) (Thread)

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

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

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

(Reply to this) (Parent)

da i s kvantorom suschestvobanija tozhe problemy. Esli realizujuschee naturalnoe chislo uzhe najdeno - to ponjatno, a esli net - to chto? naprimer neg(Con(NF))?

Polovina logikov ischet primer, drugaja polovina - naoborot, probuet dokazat' ZF |- Con(NF) ili chto esche kto-nibud' |-Con(NF).

(Reply to this) (Parent) (Thread)

Ну, так потому они и являются полуразрешимыми. Если не найдено ни реализующее число, ни основания для утверждения о его невозможности — приходится говорить "не знаю". Лично я не вижу в этом словосочетании ничего ужасного.

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

(Reply to this) (Parent) (Thread)

ja interesujus' arifmeticheskimi utverzhdenijami A takimi chto i A i ne A simmetrichny:
intuitivno ravnopriemlimy, ravnointeresny, nu i,konechno, neoproverzhimy ni v odnoj iz izvestnyx teorij.

Neuzheli Vy budete utverzhdat', chto odno iz nix-taki pravda?

(Reply to this) (Parent) (Thread)

Я утверждаю только то, для чего имею основания. Утверждение, что "одно из них таки правда", записывается формулой \(A\lor(\neg A)\). В рамках КПМС эта формула может считаться верной только в том случае, если верная какая-то из \(A\) и \(\neg A\). Пока вопрос не решён (что Вами и предполагается), приходится помалкивать в тряпочку.

Главное здесь состоит не в том, что "одна из формул таки верна", а в том, что у каждой из них есть смысл, что вопрос о верности формулы является содержательным (а не чисто формальным).

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

(Reply to this) (Parent) (Thread)

mojo "OR" - eto meta-ili.

mojo "OR" - ne vnutri formuly!

(Reply to this) (Parent) (Thread)

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

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

(Reply to this) (Parent)

Вдогонку: в конструктивной математике (в отличие от "конструктивной" в кавычках) мета-этаж вообще не выделяется. В этом просто нет смысла:

1) Математические суждения в рамках конструктивной установки столь же содержательны, сколь и метаматематические;

2) Метаматематические суждения представляют собой, по сути, математические высказывания, причём даже не очень высокой "степени сложности".

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

(Reply to this) (Parent)

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

(Reply to this) (Parent) (Thread)

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

(Reply to this) (Parent)

Зафиксирую ещё напоследок один фактик:

> В таком случае, вы, видимо, не знаете, что такое тезис Чёрча.

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

(Reply to this) (Parent)