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

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 либо от натурального ряда на конечное множество.

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

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

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

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

Привет



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

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, как будто того вовсе не существует - очень достойный для научного работника поступок, нечего сказать!). Нашли же, на кого ссылаться и чьему мнению доверять!

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

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


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