Войти в систему

Home
    - Создать дневник
    - Написать в дневник
       - Подробный режим

LJ.Rossia.org
    - Новости сайта
    - Общие настройки
    - Sitemap
    - Оплата
    - ljr-fif

Редактировать...
    - Настройки
    - Список друзей
    - Дневник
    - Картинки
    - Пароль
    - Вид дневника

Сообщества

Настроить S2

Помощь
    - Забыли пароль?
    - FAQ
    - Тех. поддержка



Пишет Misha Verbitsky ([info]tiphareth)
@ 2007-07-03 03:47:00


Previous Entry  Add to memories!  Tell a Friend!  Next Entry
Настроение: tired
Музыка:Альтернативная Космонавтика -- 5.03.1995 Дом Ученых
Entry tags:math, smeshnoe

гиперпростое множество
Среди прочего, Шень рассказал мне, что есть гиперпростое
множество.
Это рекурсивно перечислимое множество A,
обладающее следующим свойством. Обозначим
n-й (в порядке возрастания) элемент дополнения к A
за b_n. Тогда последовательность {b_n} растет
быстрее любой вычислимой функции

Числа Грэма
отдыхают, они растут ниибацца быстро,
но таки гораздо медленнее.

Еще есть максимальное множество,
это перечислимое множество A, такое, что любое
перечислимое множество, содержащее A, отличается
от A либо от натурального ряда на конечное множество.

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

Конструктивная математика!

По степени живительной бредовости эта наука круче
ультрафильтров вдесятеро. Круче и неконструктивнее:
однако явных примеров максимального множества наука,
кажется, не ведает, несмотря на многочисленные
работы, им посвященные. При взгляде на подобное
сторонники финитизма должны биться в жутком
припадке и грызть на себе гениталии. Логически
рассуждая.

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

Привет



(Читать комментарии) - (Добавить комментарий)


[info]kouzdra
2007-07-03 12:02 (ссылка)
По крайней мере лет 20-30 назад она занималась примерно вот этим вот:

http://lib.mexmat.ru/books/1268
http://lib.mexmat.ru/books/22375
http://www.amazon.com/Categorical-Theory-Studies-Foundations-Mathematics/dp/0444508538
http://lib.mexmat.ru/books/18929

etc.

И все, не все, но очень многое это как раз вполне практически в компутерщине юзается. А вовсе не вся та хрень, о которой ты говоришь и которую у нас действительно очень любят. Я собственно в этом разбирался по вполне практической надобности и то, что вместо этого на матмехе под логикой понимают рекурсивные функции, несколько бесит. Потому что, например, про современные функциональные языки без минимального представления у публики по этой теме рассказывать сложно - не объяснить откуда оно взялось и почему устроено именно так, а не иначе. Ну и много чего еще не объяснить. Это примерно как про RSA рассказывать людям, которые про простые числа не слышали.

Еще логика всякими хитрыми дедуктивными системами занимается. Тема странная, но вполне практически востребованная.

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

Для этого просто надо тему до конца доводить - рассказывать парадокс Сколема, объяснять про относительность мощности (и бесконечности) и закрывать тем, что все эти жуткие множества вообще говоря, оторванная от жизни фигня, порожденная конкретным формализмом.

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

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

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]universalist
2007-07-03 12:16 (ссылка)
>Кстати, эти треды меня вывели на совершенно умопомрачительное обсуждение, где примерно теже люди обсуждают вопросы о существовании бога, каким-то образом к тому припутав Вопенку :)

По моему Вопенка напротив стремится уязвить теорию Кантора, в которой сплошные бесконечности, а их, как сказал Больцано, может созерцать только кто?

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kouzdra
2007-07-03 12:41 (ссылка)
Так что он там пытался - это его дело, важно, что получилось почти тоже самое, только ярлычки поменялись.

(Ответить) (Уровень выше)


[info]tiphareth
2007-07-03 12:29 (ссылка)
Топосами в логике сейчас особо не занимаются,
в математике, впрочем, тоже давно их позабыли.
Это деятельность по большей части для полупомешанных,
хотя я тоже слышал, что в роботехнике топосам нашли
полезные применения.

>Для этого просто надо тему до конца доводить

Ее нельзя до конца довести, ибо актуальные темы в логике
(форсинг, колмогоровская сложность, P/NP) требуют года-двух
минимум, а в математике никак не применяются.

Такие дела
Миша

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kouzdra
2007-07-03 12:38 (ссылка)
хотя я тоже слышал, что в роботехнике топосам нашли полезные применения

Там на самом деле сейчас дедуктивным системам нашли применение. Причем важное. А топосы и т.п. там вылезают поскольку тема смежная.

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

Ее нельзя до конца довести, ибо актуальные темы в логике (форсинг, колмогоровская сложность, P/NP) требуют года-двух минимум, а в математике никак не применяются

Дело в том, что они и в компьютерщине толком не применяются.

(Ответить) (Уровень выше)


[info]kouzdra
2007-07-03 12:44 (ссылка)
PS: Кстати - главная ошибка ныншених "конструктивистов", по крайней мере из тех тредов - это что они думают, что от того, что объект "бесконечный", его в компьютер сложнее запихивать.

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

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]tiphareth
2007-07-03 12:49 (ссылка)
Это Гастрит, он никакой не конструктивист,
а человек, страдающий философской одержимостью.

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

Такие дела
Миша

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kouzdra
2007-07-03 13:57 (ссылка)
Я лично думаю. что нет, в частности потому, что большую часть всей этой кардинальной фигни можно из нее исключить гарантировано непротиворечивым способом. Да наверное и от самой теории множеств можно как-нибудь уйти на что-то менее навороченное. В те же категории позаталкивать. Там ZF юзается довольно ограниченно. Только никто даже этого делать не будет, а уж тем более - на конструктивный вариант переходить.

(Ответить) (Уровень выше)


[info]http://users.livejournal.com/__gastrit/
2007-07-03 17:09 (ссылка)
Против "философской одержимости" возражать не буду, а вот про "никакой не конструктивист" интересно. По каким признакам Вы отличаете "настоящего" конструктивиста от липового? И много ли "настоящих" Вы вообще видели?

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

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]tiphareth
2007-07-03 17:21 (ссылка)
Видел Шеня, Успенского и Семенова
(ходил на семинар "Колмогоров, Семенов, Шень",
года 2 или 3). Разборова видел пару раз.

>По каким признакам Вы отличаете "настоящего" конструктивиста

По наличию опубликованных научных работ по теме

Такие дела
Миша

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]tiphareth
2007-07-03 17:36 (ссылка)
>"Колмогоров, Семенов, Шень"

Все-таки "Колмогоров, Успенский, Шень" скорее всего

(Ответить) (Уровень выше)


[info]http://users.livejournal.com/__gastrit/
2007-07-03 18:04 (ссылка)
Успенский - это которому принадлежит фраза «я считаю Маркова выдающимся математиком, но его конструктивистскую деятельность не могу расценивать иначе как вредную»? Ну-ну, скажите-ка ему самому, что он конструктивист - интересно, куда он после этого Вас пошлёт :-))

Все упомянутые Вами лица - это специалисты по теории рекурсии, развиваемой в рамках и средствами "классической" теоретико-множественной математики. Конструктивистом никто из них не является, т.к. конструктивизм - это как раз разновидность "философской одержимости": «конструктивное направление в математике — математическое мировоззрение, связанное с признанием исследования конструктивных процессов и конструктивных объектов основной задачей математики» (Марков). Не верите - проконсультируйтесь у того же Шеня.

> По наличию опубликованных научных работ по теме

Хороший критерий! Где можно посмотреть работы указанных авторов по УДК 510.25?

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

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]tiphareth
2007-07-03 18:21 (ссылка)
>работы указанных авторов по УДК 510.25

Помочь не могу, увы: я в Москве, и MathSciNet у меня нет.

>признанием исследования конструктивных процессов и
>конструктивных объектов основной задачей математики

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

Такие дела
Миша

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]http://users.livejournal.com/__gastrit/
2007-07-03 18:54 (ссылка)
> По мнению людей, которые в теме,
> подобные заявления только дискредитируют предмет.

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

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

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]tiphareth
2007-07-03 19:42 (ссылка)
>Кстати, вот Вам и безошибочный тест на
>"конструктивистскость": если человек считает "подобные
>заявления" дискредитирующими предмет - то он точно не
>конструктивист.

Это, в принципе, два совершенно разных значения одного
слова: конструктивизм как религиозная конфессия (ваш
случай) и конструктивизм (теория рекурсии) как одна из
частей логики и оснований. Интересно, что пересекаются
они весьма редко: не думаю, что кто-то из ныне
практикующих эту науку математиков подпишется под
словами Маркова.

Такие дела
Миша

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]http://users.livejournal.com/__gastrit/
2007-07-03 20:12 (ссылка)
Везде, где я встречал термин «конструктивизм», этим термином обозначалась именно "конфессия". Вам известны другие источники? Был бы признателен, если бы Вы их указали.

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

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]tiphareth
2007-07-03 21:49 (ссылка)
Сколько угодно.

Errett Bishop,

"Schizophrenia in contemporary mathematics"

(A) Mathematics is common sense;
(B) Do not ask whether a statement is true until you know what it means;
(C) A proof is any completely convincing argument;
(D) Meaningful distinctions deserve to be preserved.

* * *

Bishop E: `Foundations of constructive analysis', McGraw-Hill, 1967.

"We are not contending that idealistic mathematics is worthless from the
constructive point of view. This would be as silly as contending that
unrigorous mathematics is worthless from the classical point of view.
Every theorem proved with idealistic methods presents a challenge: to
find a constructive version, and to give it a constructive proof."

* * *

E.B. Davies
A DEFENCE OF MATHEMATICAL PLURALISM
http://www.mth.kcl.ac.uk/staff/eb_davies/postsubmission91.pdf

Привет

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]http://users.livejournal.com/__gastrit/
2007-07-04 14:42 (ссылка)
О Бишопе я уже достаточно сказал в другом посте, теперь добавлю кое-что о Дэвисе. Тем более, что это будет кореллировать со старой темой "колония-метрополия".

Базовые результаты в области конструктивного анализа получены в конце 1940-х и начале 1950-х годов в школе Маркова (за исключением некоторых ещё более ранних, вроде последовательности Шпекера). Опубликовано всё это в 1958-62 годах в «Трудах МИАН». Найдите, будьте любезны, у Дэвиса хоть одну ссылочку на Цейтина (у которого, например, отдельная статья была про теоремы о среднем — причём упоминаемая Дэвисом конструкция с $\log(1+x^{n})$ по сути ничем не отличается от цейтинских трёхзвенных ломаных, кроме чуть большей мутности изложения идеи), или на Шанина (опус которого про конструктивные функциональные пространства даже был в своё время переведён "белыми людьми" из AMS). Не найдёте. Так что поздравляю: Вы сами же привели пример того, как "метрополия" кормится за счёт плагиирования результатов "помойной рашки".

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

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]tiphareth
2007-07-04 14:55 (ссылка)
Да подобных примеров - миллион. До 1990-го
в России делалось процентов 30 мировой математики.

Но после 1990-х практически все люди, способные
делать исследования мирового уровня, уехали.

Такие дела
Миша

(Ответить) (Уровень выше)


[info]m
2007-07-03 18:01 (ссылка)
конструктивная математика (скорей, правда, интуиционистская)---это та, которую можно делать в любом топосе))

(Ответить) (Уровень выше)


[info]universalist
2007-07-03 13:43 (ссылка)
>объект "бесконечный", его в компьютер сложнее запихивать.


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

(Ответить) (Уровень выше)

Раз уж зашёл, обозначу присутствие
[info]http://users.livejournal.com/__gastrit/
2007-07-03 17:00 (ссылка)
> На самом деле в компьютер должно быть удобно запихивать формализм,
> с помощью которого объект описывается.

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

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

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]kouzdra
2007-07-03 17:11 (ссылка)
Реально машина орудует электрическими зарядами в конденсаторах и т.п.

Всему остальному смысл придается намерениями программистов и интерпретацией результатов. А это могут быть и формупы теории, и числа и геометрические фигуры - что угодно. На каком-то уровне, например, это никакие не "формулы теории" а объекты, если язык ОО, или лямбда-выражения и рекурсивные типы, если FP.

Но если программая занимается например вычислениями - то она оперирует числами. Если формальным выводом - то формулами.

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

для противоречивой теории и в принципе невозможно

Да почему же невозможно - противоречивость теории не очень мешает ее практическому применению. Тот же матан известных времен взять или теорию множеств. Так же как и алгоритмическая неразрешимость задачи не особенно мешает ее запизиванию в компьютер. А разрешимость - не особенно помогает :)

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]http://users.livejournal.com/__gastrit/
2007-07-03 18:45 (ссылка)
> Реально машина орудует электрическими зарядами в конденсаторах и т.п.

И ими тоже не орудует. Конденсатор состоит из атомов, атомы - из электронов с нуклонами, электрический заряд - это проявление взаимодействия электронов с фотонами, которые и т.д. Короче, машина не орудует ничем, ибо ничего на деле не существует, а всё вокруг - пустота :-))

Так что софистику наводить и я умею. Но вот того факта, что при определённых условиях "заряды в конденсаторах" реально ведут себя как 0 и 1, а сочетания таких "зарядов" - как булевы векторы, это не отменяет.

> это могут быть и формупы теории, и числа и геометрические фигуры - что угодно.

Правильно, и черти с рогами - тоже. Что мешает аксиоматизировать демонологию, а затем внедрить в неё машинные выводы? Ровно ничего. А вот почему этого не делается (либо делается маргиналами, про которых мало что слышно)? Да ровно потому, что в реальное существование чертей сегодня мало кто верит: неинтересны людям "формализации" несуществующих явлений! С актуально бесконечными множествами картинка на деле схожая: в действительности их не существует, и все ZF и NBG - это те же самые формальные демонологии. Однако принято считать, что они есть, а потому результаты получаемых в рамках ZF выводов имеют некое реальное значение (отличное от констатации "в рамках теории такой-то мне удалось вывести то-то"). Как раз это обстоятельство меня, в частности, и не устраивает.

> На каком-то уровне, например, это никакие не "формулы теории" а объекты,
> если язык ОО, или лямбда-выражения и рекурсивные типы, если FP.

К чему это было? Сказанное Вами означает только одно: объекты в C++ и бинарные деревья в LISP'е - это реально существующие вещи. В отличие от актуально бесконечных множеств и чертей с рогами.

> С точки зрения парадокса Сколема можно считать, что и теория множеств оперирует формулами

"С точки зрения парадокса Сколема" надо сначала иметь для этой теории модель - а где таковая для ZF?

> Да почему же невозможно - противоречивость теории не очень мешает
> ее практическому применению. Тот же матан известных времен взять

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

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

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]kouzdra
2007-07-03 19:23 (ссылка)
Что мешает аксиоматизировать демонологию, а затем внедрить в неё машинные выводы? Ровно ничего. А вот почему этого не делается (либо делается маргиналами, про которых мало что слышно)?

Потому что это, вроде бы, никому не нужно. Впрочем - не удивлюсь, если кто-нибудь и сделал.

К чему это было? Сказанное Вами означает только одно: объекты в C++ и бинарные деревья в LISP'е - это реально существующие вещи. В отличие от актуально бесконечных множеств

FP - это давно не Lisp и не бинарные деревья. Но я не вполне понимаю почему скажем список из всех натуральных чисел существует (в Haskell, например, он записывается как [1..]), а множество всех натуральных чисел - не существует.

"С точки зрения парадокса Сколема" надо сначала иметь для этой теории модель - а где таковая для ZF?

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

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

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

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]dmitri83
2007-07-03 19:50 (ссылка)
?? Теорема Лёвенгейма-Сколема рассказывает, как построить счётную модель по уже существующей, данной модели теории. В случае ZF ещё никто никогда не видел явно построенной её модели, несчётной ли, счётной ли.

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]kouzdra
2007-07-03 20:08 (ссылка)
Она не по модели ее строит. Там "объектами" модели являются формулы теории, описывающие существование объектов. Точнее - классы эквивалентности таких формул. То есть, конечно, сама теорема доказывается в рамках ZF, что несколько забавно выглядит, но в модели ничего особенно неконструктивного нету

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]dmitri83
2007-07-03 22:06 (ссылка)
а, в этом доказательстве, с witnesses, да (я сперва подумал про другое, когда строится элементарная подмодель). Хм, никогда не думал об этом. Всё равно, пользы от этой процедуры для построения осязаемой модели ZF мало. Там есть момент в доказательстве, где используется то, что теория полна. ZF не полна, и для того, чтобы её расширить её до полной теории, надо либо предъявить модель (круг замкнулся), либо воспользоваться чем-то вроде аксиомы выбора.

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]kouzdra
2007-07-03 22:42 (ссылка)
Там непротиворечивость нужна. Но она всегда нужна. А аксиома выбора там если я ничего не путаю, на счетном (и упорядоченном) множестве ни на фиг не нужна.

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]dmitri83
2007-07-04 00:09 (ссылка)
Полнота нужна, иначе не получится доказать, что построенная модель есть модель нашей теории.

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

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]tiphareth
2007-07-04 01:22 (ссылка)
Ну, в принципе, если нужна счетная модель теории множеств,
можно обойтись геделевским универсумом
http://en.wikipedia.org/wiki/Constructible_universe
куда уж конструктивнее

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]dmitri83
2007-07-04 13:34 (ссылка)
То, что L является моделью теории множеств, опирается на существование large cardinals. Либо, можно построить L внутри какой-то другой модели теории множеств, но тогда надо, чтобы свыше дали эту модель.

Собственно, чудес не бывает, из-за соответствующей теоремы Гёделя. Чтобы построить модель ZF надо уверовать во что-то более сильное: в непротиворечивость ZF, в существование large cadinals или что-то ещё.

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]tiphareth
2007-07-04 14:45 (ссылка)
Ну, из непротиворечивости ZFC [info]kouzdra и исходил
а независимость L=V от ZFC кажется, доказана

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]dmitri83
2007-07-04 15:27 (ссылка)
Я неточно выразился. Как выяснилось чуть выше, просто поверить в непротиворечивость недостаточно, например, способ построения модели с помощью теоремы Лёвенгейма-Сколема, про который говорит [info]kouzdra, не позволяет получить конкретного описания модели. Может какие-то другие способы есть, но про них неизвестно. Выше же в разговоре, насколько я понял, речь шла об описании модели настолько конкретном, чтобы можно было запихнуть его в компьютер.

И кстати, конструктивный универсум тоже является сомнительным кандидатом на такое описание (это ещё при том, что надо принять существование больших кардиналов): как мы будем итерировать на компьютере конструкцию L_\kappa до какого-то недостижимого кардинала, не очень понятно.

Резюмируя: максимум, с чем мы можем работать на компьютере, это с формулами и доказательствами в рамках ZFC, но не с моделями.

а независимость L=V от ZFC кажется, доказана

Не понял, причём тут независимость L=V от ZFC?

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]tiphareth
2007-07-04 15:32 (ссылка)
При том, что конструктивный универсум является моделью для
ZFC+L=V, если я ничего не перепутал

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]dmitri83
2007-07-04 15:35 (ссылка)
Ну да, является.

(Ответить) (Уровень выше)

Re: Раз уж зашёл, обозначу присутствие
[info]kouzdra
2007-07-04 15:59 (ссылка)
Зачем там полнота? Она просто по построению является моделью. Другое дело, что довольно ограничительной моделью - у ZF например она не будет содержать никаких "экзотических" объектов. Будет я думаю, примерно (или даже точно) соотвествовать AZ+аксиома конструктивности.

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]dmitri83
2007-07-04 16:06 (ссылка)
когда вы доказываете (индукцией по структуре формулы), что формулы теории истинны в построенной модели, вы используете полноту.

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]kouzdra
2007-07-05 00:42 (ссылка)
Каким образом? Тем более, что полных теорий в реальной жизни можно считать не бывает.

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]dmitri83
2007-07-05 03:01 (ссылка)
ну, откройте любое доказтельство. Чтобы сделать шаг по индукции нужно, чтоб \phi \notin T iff \neg \phi \in T и прочая подобная ерунда, которая следует из полноты T.

Полные теории ещё как бывают (например, плотные линейные порядки, алгебраически замкнутые поля заданной характеристики, real closed fields, random graph). Теория моделей только ими и занимается.

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]kouzdra
2007-07-05 10:40 (ссылка)
Доеду до дому и посмотрю я уже чего-то засомневался, но afaik вы не правы.

Что до полных теорий конечно, но только теория моделей занимается не ттолько ими. Собственно почти все доказательства независимостей и проч. - теоретико-модельные.

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]dmitri83
2007-07-05 13:52 (ссылка)
Уж позвольте, когда я говорю "теория моделей", я под этим подразумеваю именно теорию моделей :) Ту область, в которой доказательства независимости, называют теорией множеств.

(Ответить) (Уровень выше)

Re: Раз уж зашёл, обозначу присутствие
[info]kouzdra
2007-07-08 23:34 (ссылка)
Открыл. Даже несколько. Полнота теории не нужна.

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]dmitri83
2007-07-09 02:23 (ссылка)
не верю, я думаю, я ещё не впал в маразм и в этих трёх соснах не заблужусь )
и где такое доказательство?

вот построена модель M из констант. Предполагаем T полной и доказываем по индукции, что M |= \phi iff \phi \in T. Атомарные формулы верны по построению. Предположим, что \neg \phi \in T и уже доказали утверждение для \phi, поскольку \phi \notin T (которая полна), то M \notmodels \phi, или M |= \neg \phi. Если же полноту T не предполагать, то может быть, что хоть \phi \notin T, но при этом M |= \phi. И как тут что-то доказывать?

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]kouzdra
2007-07-12 15:42 (ссылка)
Я наконец добрался до книжки Коэна - мне казалось, что там другое доказательство. Нет - тоже самое, только более элементарное:

Собственно теорема Л-С исходит из наличия модели и строит счетную просто вводя константы для выполнимых формул вида А(x, y1, y2..., yn) (индукцией по n и объединением получившихся множеств). Доказательство того, что это модель, идет индукцей по числу кванторов в формулах.

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

У Клини оценка мощности модели дается просто в теореме о полноте, и утверждается что первоначальное доказательство Л-С было примерно таким же.

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]dmitri83
2007-07-12 15:47 (ссылка)
Наличие модели функционально ничем с точки зрения доказательства не отличается от полноты теории.

Именно, и ни того, ни другого мы "пощупать" не можем. Поэтому я удивился там в самом верху, когда вы написали, что с помощью теоремы Л-С, мол, можно легко построить модель теории множеств. Если бы можно было, тогда бы все теоремы теории множеств не начинались славами "предположим, что ZF непротиворечива и у неё есть модель M".

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]kouzdra
2007-07-12 15:52 (ссылка)
Я говорил, что можно построить счетную модель, "содержательный" смысл которой довольно конструктивен - константы соотвествуют формулам теории. Конечно только в предположении непротиворечивости.

А так - разумеется формального доказательства непротиворечивости ZF быть не может - просто по теореме Геделя.

предположим, что ZF непротиворечива и у неё есть модель M

Достаточно непротиворечивости. Существование модели вытекает из теоремы о полноте.

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]dmitri83
2007-07-12 15:56 (ссылка)
Ну какая же тут конструктивность, константы надо отфакторить по отношению эквивалентности, которое определяется теорией, которую никак конструктивно описать нельзя (какое-то полное расширение ZF).

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]kouzdra
2007-07-12 16:04 (ссылка)
Эквивалентность там не надо - это меня взглючило. Просто представителя из модели выбрать для каждой выполнимой бескванторной формулы и уже выбраных значений ее аргументов, кроме первого. В таком варианте AC конечно нужна.

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]dmitri83
2007-07-12 16:16 (ссылка)
Факторить придётся, если в сигнатуре есть равенство (в случае ZF есть). И да, там и без этого всё зависит от полноты теории.

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]kouzdra
2007-07-12 16:27 (ссылка)
Там не надо факторить - просто будет несколько представителей в модели для по сути одной и той же формулы. Если их несколько в "базовой". А полнота там не требуется.

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]dmitri83
2007-07-12 16:31 (ссылка)
Замечательно, будет две константы для формулы \phi(x), а в теории тем временем будет формула "\phi(x) верна ровно на одном элементе модели".

Почему это полнота не потребуется? Как отсутствие факторизации влияет на довод, что я приводил выше (что не получится доказать выполнение формул теории на модели)?

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]kouzdra
2007-07-12 16:33 (ссылка)
Если их было две в исходной модели - эта формула не может быть верна. А если она верна - константа и так окажется одна и та же.

А зачем там полнота?

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]dmitri83
2007-07-12 16:46 (ссылка)
Погодите, мы про какое доказательство говорим? Я думал про "синтаксическое", которое от теории отталкивается.

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

По-моему, мы пошли по кругу.

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]kouzdra
2007-07-12 16:57 (ссылка)
В точном смысле "констуктивной математики" там, конечно, ничего не доказать. В смысле же интерпритации - таки да - модель строится из формул (точней - констант, которые этим формулам соотвествуют). Просто непонятно, какой смысл при этом остается у "конструктивных" философствований, когда и так известно, что формально доказать непротиворечивость нельзя - хоть конструктивно, хоть в ZF, а никаких метафизических бесконечностей и прочей лабуды в счетной модели нет.

PS: Если интересно, могу доказательство из Коэна закинуть - оно всего на страничку и он у меня есть в электронном виде

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]dmitri83
2007-07-12 17:05 (ссылка)
В смысле же интерпритации - таки да - модель строится из формул (точней - констант, которые этим формулам соотвествуют).

Множества формул тоже могут быть очень сложно устроены, будь даже формул счётное количество.

PS: Если интересно, могу доказательство из Коэна закинуть - оно всего на страничку и он у меня есть в электронном виде.

спасибо, вряд ли я там для себя что-то новое открою )

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]kouzdra
2007-07-12 17:12 (ссылка)
Множества формул тоже могут быть очень сложно устроены, будь даже формул счётное количество

Да это понятно - я вон по следам того трепа в [info]ru-lambda@lj обсуджение списков затравил - тоже весьма сложно устроенные объекты. И конструктивнее некуда - реальные совершенно объекты в реальных программах :)

(Ответить) (Уровень выше)

Re: Раз уж зашёл, обозначу присутствие
[info]http://users.livejournal.com/__gastrit/
2007-07-03 20:05 (ссылка)
> я не вполне понимаю почему скажем
> список из всех натуральных чисел существует
> (в Haskell, например, он записывается как [1..]),
> а множество всех натуральных чисел - не существует.

А я вот не вполне понимаю, почему в случае действительного существования списка натуральных чисел в Haskell проблема нечётных совершенных чисел до сих пор числится открытой. Список-то допускает полный перебор!

С Haskell'ом не работал, врать не буду. Но вот что объект, записываемый как [1..], является "списком натуральных чисел" разве что по названию - уверен железно. Свойства у него - не те же, что у "настоящих" списков.

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

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


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

А вот это правильно! Теория о сношениях человека с дьяволом имела практические применения в избытке: ведьм реально жгли по всей Европе. Следовательно, каждое слово в «Malleus maleficarum» истинно. Брависсимо!

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

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]tiphareth
2007-07-03 20:08 (ссылка)
"Истинно" и "ложно" - слова-паразиты.
Любое утверждение истинно в одном контексте,
ложно в другом, бессмысленно в третьем.

(Ответить) (Уровень выше)

Re: Раз уж зашёл, обозначу присутствие
[info]kouzdra
2007-07-03 20:20 (ссылка)
А я вот не вполне понимаю, почему в случае действительного существования списка натуральных чисел в Haskell проблема нечётных совершенных чисел до сих пор числится открытой. Список-то допускает полный перебор!

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

А [0..] - это просто сокращение для кода вроде:
let nat n = n:nat (n+1) in nat 1
a:b - это список с головой a и хвостом b

По машинному представлению ничем не отличается от прочих списков.

Честно говоря, не очень понятно, как её "кодировать в машине". Было бы очень неплохо это уточнить

Ну там содержательный смысл ее в том, что объектами модели являются формулы теории вида "существует и единственное X, такое что ...". Точнее - классы эквивалентностей этих формул. А у Барвайса - обобщенная теорема, на случай теорий не со счетным, как у ZF множеством аксиом, а произвольным.

А вот это правильно! Теория о сношениях человека с дьяволом имела практические применения в избытке: ведьм реально жгли по всей Европе. Следовательно, каждое слово в «Malleus maleficarum» истинно.

Я хоть слово говорил об истинности?

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]http://users.livejournal.com/__gastrit/
2007-07-03 21:05 (ссылка)
Список, насколько моя знать, это объект, удовлетворяющий следующему индуктивному определению:

1) Пустой список есть список.
2) Если L - список, а t - объект, могущий быть элементом списка рассматриваемого вида, то результат "приписывания" t к L - тоже список.

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

А не в стороне - то, что Вы своё [0..] к пустому списку заведомо не редуцируете. И потому свойства Вашего [0..] ох как отличны от "списочных": для любого разрешимого свойства N натуральных чисел свойство «список содержит элемент со свойством N» тоже разрешимо, а вот свойство «нечто вроде [0..] содержит элемент со свойством N» - уже неразрешимо!

Об этом же я и писал в старых околоконструктивистских баталиях, на которые Вы тут ссылались: описать-то бесконечный класс объектов (средствами вроде Вашего [0..] или даже ещё более навороченными) можно - вот только считать, что с этим описанием потом можно работать как с авоськой картошки (допускать полный перебор, считать все вопросы разрешимыми), уже нельзя. А в ZF именно так и считают.

> Точнее - классы эквивалентностей этих формул.

Так "формулы" или "классы эквивалентности"? Вопрос не праздный: класс эквивалентности по неразрешимому отношению - это, вообще-то, "объект" совершенно неконструктивный и в машину не загоняемый.

> Я хоть слово говорил об истинности?

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

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

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]kouzdra
2007-07-03 21:22 (ссылка)
Суть этого определения в том, что любой "реальный" список можно эффективно "раздеть" до пустого

Если Вы внимательно посмотрите на свое определение - то убедитесь, что это неверно. Пример Вам только что был предъявлен.

эффективное на машине с одним объёмом памяти и быстродействием может быть неэффективно на другой

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

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

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

Вопрос не праздный: класс эквивалентности по неразрешимому отношению - это, вообще-то, "объект" совершенно неконструктивный и в машину не загоняемый

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

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

Я знаю, что ZF безусловно является практически полезным инструментом, и склонен думать, что она скорее всего непротиворечива. И что даже если она окажется противоречива, проблему это создаст скорее технического рода. Как уже было с канторовской теорией. А что значит "ZF истинна" я не понимаю.

(Ответить) (Уровень выше)

Re: Раз уж зашёл, обозначу присутствие
[info]tiphareth
2007-07-04 01:12 (ссылка)
>описывать свойства реально существующих объектов

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

Умозрительность ультрафильтров - явление более грубого
порядка, но природа этой умозрительности та же.

Я не выступаю за ультрафинитизм, но призрачность
объектов, с которыми мы имеем дело - печальный
факт, с которым приходится мириться. Следуя заветам
Бишопа:

"We are not contending that idealistic mathematics is worthless from the
constructive point of view. This would be as silly as contending that
unrigorous mathematics is worthless from the classical point of view.
Every theorem proved with idealistic methods presents a challenge: to
find a constructive version, and to give it a constructive proof."

Такие дела
Миша

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: Раз уж зашёл, обозначу присутствие
[info]http://users.livejournal.com/__gastrit/
2007-07-04 14:16 (ссылка)
> "Максимальное множество" из корневого поста
> ничуть не менее умозрительно, чем какие-нибудь
> экзотические счетные ординалы.

См. Х. Роджерс, Теория рекурсивных функций и эффективная вычислимость, §12.4. Почему конкретный перечисляющий алгорифм является "не менее умозрительным", чем доказательства чистого существования — сие для меня непостижимо.

> Непротиворечивость математики, которая включает
> "максимальные множества", столь же неочевидна,
> как непротиворечивость математики,
> включающей числа Грэма.

Поясняю свою позицию: мне плевать на непротиворечивость с высокой колокольни. За этим, пожалуйста, к Гильберту и Co. Для меня же главное — наличие конкретного, фактического, объекта исследования. В конструктивной математике таковой есть, в теоретико-множественной — нет.

> призрачность объектов, с которыми мы имеем дело -
> печальный факт, с которым приходится мириться.
> Следуя заветам Бишопа

Это ваш Бишоп, кстати, являлся в 1966 году на конгресс в Москву и пытался там договориться с Марковым. Кушнер описывает (http://cshistory.nsu.ru/obj2964/INTERFACE.htm), чем эта попытка окончилась. Бишоп поступил гениально: решил, как двухлетний ребёнок, побить пол, о который ударился (перестал замечать оказавшийся его слабой головке не по зубам soviet constructivism, как будто того вовсе не существует - очень достойный для научного работника поступок, нечего сказать!). Нашли же, на кого ссылаться и чьему мнению доверять!

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

(Ответить) (Уровень выше)


(Читать комментарии) -