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

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]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 обсуджение списков затравил - тоже весьма сложно устроенные объекты. И конструктивнее некуда - реальные совершенно объекты в реальных программах :)

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


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