НГУ

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

Если же ввести то ограничение (которое в тюремных терминах означает совпадение натуральных и внатуральных чисел), то в результате получится теория, состоящая из всех предложений, истинных в моделях ZFC c "истинными" натуральными числами.
Согласен. Хочется как-то регламентировать класс "законных" рассуждений на синтаксическом уровне. В случае успеха тут неизбежно возникнет какое-то необычное понятие доказательства, так как в классическом смысле ни тюремная теория, ни теория моделей с "истинными" натуральными числами не аксиоматизируемы.
Опять согласен. По сравнению с ZFC тюремная теория "еще более неполная": имеется еще больше таких формул \phi, что ни \phi, ни ~\phi не являются тюремами.
Т.е. речь идет все же о теории, состоящей из предложений, истинных в моделях с "истинными" натуральными числами?

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

>аксиома о существовании множества натуральных чисел, о которой >Вы говорили,

\exists X \forall x [x \in X <P>конечно же должна у нас быть.

Интересно, что дополнительно дает эта аксиома ?

Глядя на Ваш смайлик, я подозреваю, что утверждение этой аксиомы кажется Вам с очевидностью выполненным. Если я угадал, то вынужден разочаровать: оно не выводится из остальных аксиом. Иными словами, существуют модели, в которых утверждения остальных аксиом истинны, а утверждение этой аксиомы -- ложно.

Я думаю, что формула

exists X \forall x [x \in X <=> P(x)]

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

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

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


Наши упорные беседы навели меня в конце концов на одну новую мысль. У нас есть, например, слабая монадическая логика второго порядка, которая расширяет обычную логику. В ней можно брыть кванторы по конечным множествам элементов модели: писать
\exists Y A(x,Y),
которая верна тогда и только тогда, когда найдётся конечное множество элементов модели Y, для которого A(x,Y) верна. Что, интересно, будет, если аксиомы теории множеств формулировать на её языке? По крайней мере, непонятно, что может ухудшиться. Истинные натуральные числа в ней легко определяются.

_________________
Не беги от снайпера - умрёшь усталым

Для меня и суть предшествующей части дискуссии так и не дошла, но вот это убило совсем:Дык кто нам априори скажет, какие множества в модели являются конечными?..

Нормальным -- это каким? "Истинным"? Мы по-прежнему хотим, чтобы в моделях все натуальные числа были "истинными"? Если бы каким-то чудом родился синтаксический аппарат (или нечто вроде позитивного теста) для теории, состоящей из предложений, истинных в моделях с "истинной натуральностью" (назовем ее теорией TN), то наступило бы счастье?
А для этой логики сущестует позитивный тест общезначимости? Ведь без него она ничем не лучше теории TN. Далее, захотим ли мы, чтобы конечность второго порядка совпадала с конечностью первого порядка? Если захотим, то мы фактически опять вернемся к TN.

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

О, свежая голова! Сейчас мы замутим всё по-новой. Постановка-то проблемы ясна (см. заголовок темы)?

Ещё раз старый пример в чуть иной постановке: у нас есть очень сообразительный человек, который всю жизнь прожил на Антарктиде, и ничего не слышал про математику. Мы решили по электронной почте сообщить ему о ней, и начать с общепризнанного основания математики - теории множеств.

Мы примерно растолковали ему, что множества - это совокупности объектов, привели примеры множеств 0, 1={0}, 2={0,1} и ещё нескольких, а потом объяснили, как с их помощью можно считать число предметов. Затем сообщили ему аксиомы ZFC - те законы, которые этими множествами управляют. А потом сказали, что натуральные числа - это множества, которые удовлетворяю формуле nat(x).

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

_________________
Не беги от снайпера - умрёшь усталым

Дык нет, это-то я все как раз понял. Я не понял, кого Вы, Павел, тут подкалываете с применением компактности в самом первом постe; ведь "определение" множества натуральных чисел содержит счетную дизъюнкцию (корректность которой специально внесена в список аксиом ZF, насколько я помню). Однако, принимая во внимание, что обычно Вы поднимаете вполне серьезные темы, я начинаю думать,что это я чего-то не понимаю; вот я и не могу понять, чего же именно...

P.S. Блин, глюки какие-то; все форумы вчера нормально просматривались, но не отвечались ни в какую...

_________________
КТО ИЩЕТ СМЫСЛ - ТОТ ГЛЯДИТ НА НЕБЕСА...

А что это за зверь -- "корректность счетной дизъюнкции в ZF"? (Не припоминаю такого.)

Я тоже не совсем Вас понял: взяв ближайшую книжку, содержащую ZFC (это оказался задачник Лаврова-Максимовой), прочёл в ней следующее.

В параграфе 7 части II указан список аксиом ZF. Сразу за ним идут некоторые формулы, в частности, формулы
x=\omega и N(y) (как y \in \omega)
которые как раз определяют множество натуральных чисел и сами натуральные числа (впрочем, последнее в явном виде не утверждается). Никаких счётных дизъюнкций в них нет. На самом деле, их там и не должно быть - ZFC ценна для нас возможность строить конечные выводы формул, и мы не должны выходить за рамки логики 1-го порядка.

_________________
Не беги от снайпера - умрёшь усталым

Э-э-э, что-то я слишком коряво изложил свою мысль... Однако, исправляться будет дольше, чем посмотреть Лаврова - Максимову (благо, Павел только номер строки не указал). :) Может, меня, наконец и расклинит... ;)

_________________
КТО ИЩЕТ СМЫСЛ - ТОТ ГЛЯДИТ НА НЕБЕСА...

На свете, как известно, счастья нет, но есть покой и воля.


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

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

Если эта проекция совпадает с ZFC, то, спрашивается, какая с неё польза. А если она больше, чем ZFC, то мы тем самым предлагаем как минимум добавить к ZFC какие-то новые аксиомы. Возникает вопрос, почему бы не начать просто с их добавления, не выходя на рамки первого порядка, и, главное, что это за аксиомы, и чем они хороши. И там, и там проблемы.

_________________
Не беги от снайпера - умрёшь усталым

Однака ZF(C) - логика второго порядка.