Someone писал(а):
Котофеич, у нас с Вами разногласие-то не в формулировке теоремы Гёделя о полноте. Она формулируется так (Е.Расёва, Р.Сикорский. Математика метаматематики. "Наука", Москва, 1972, глава VIII, § 5, пункт 5.3):
Каждая непротиворечивая теория с не более чем счётным множеством математических аксиом имеет счётную семантическую модель.
Слово "семантическая" означает, что функция истинности принимает значения в двухэлементной булевой алгебре.
У Коэна сфомулирована и доказывается более общая теорема, не требующая счётности множества математических аксиом, которая в упомянутой мной книге находится в § 9 главы VIII, пункт 9.3.
Различие между теоремами 5.3 и 9.3 состоит в том, что теорему 5.3 можно доказать без аксиомы выбора, в то время как теорема 9.3 без аксиомы выбора не доказывается.
Модели можно строить из разного "материала", в частности, используя в качестве такового термы языка теории (тут возникает понятие канонической реализации языка). Я не понимаю, где, по Вашему мнению, существуют эти термы (и всё прочее, нужное для построения языка теории: алфавит, формулы, аксиомы). Как будто бы Вы считаете, что они существуют то ли сами по себе, то ли в той теории, которую Вы формализуете.
С общепринятой точки зрения, алфавит теории, её термы, фомулы и аксиомы являются элементами метатеории. Должны же мы иметь какие-то средства для описания языка и для проведения доказательства? Или мы построим язык и модель "из ничего"? П.Дж.Коэн в своей книге (Теория множеств и континуум-гипотеза. "Мир", Москва, 1969) в начале § 4 главы I говорит в связи с теоремой Гёделя о полноте: "Это рассмотрение будет проведено в традиционном математическом духе, т.е. не в рамках какого-либо формального языка. Мы воспользуемся некоторыми элементарными понятиями теории множеств. Конечно, после того, как будет формализована сама теория множеств, можно будет и это рассмотрение выразить в её формальной системе." Это означает, что в качестве метатеории берётся неформализованная теория множеств.
Сами по себе разговоры о том, что некая совокупность является множеством, да ещё счётным (или наоборот - несчётным), предполагают, что имеется некоторая теория множеств, элементом которой является упомянутое множество. Если говорится о том, что множество аксиом теории является счётным, значит, метатеория является теорией множеств. Тем более, если ещё упоминается аксиома выбора.
Использование метатеории является таким общим обстоятельством, что слово "метатеория" может даже и не упоминаться. В книге "Математика метаматематики" необходимость и роль метатеории обсуждается в § 1 главы V, но далее слово "метатеория" употребляется довольно редко. Это не означает, что метатеория не нужна. Это означает, что нет нужды всё время её упоминать, но иногда такая потребность возникает. Например, в § 3 той же главы, где обсуждается структура языка формализованной теории, говорится: "Знаки ( , ) нужно отличать от знаков ( , ). Первые - это скобки формализованной теории, вторые - метатеории для этой теории".
Нету у нас никаких разногласий, это чисто терминологические вещи.
Во первых та формализация о которой там говориться не связана с
принципиальной необходимостью обязательно различать теорию и метатеорию. Это необходимо только
для
корректного построения алгебры Линденбаума-Тарского. Там есть пример из теории групп--и ясно сказано, что какие скобки не используй хоть такие (, ), а хоть такие [, ] или даже такие
,
то в самой теории групп ровным счетом ничего не меняется.
Бо ежели она эта теория будет противоречива с
метаскобками (, ), то противоречие
мгновенно будет и в самой формальной теории с
неметаскобками [, ] . Это очевидно,
для теории групп, а для теории множеств может и не совсем очевидно, потому что аксиомы
намного сложнее. Обращаю Ваше внимание, что авторы не говорят что если языки перепутать, то случиться противоречие или что либо непоправимое в этом роде.
Ну хорошо. Я ничего против Ваших взглядов не имею и могу стать на эту точку зрения,
которую внушил когда то всем Тарский. Если Вы учились по этим книжкам, можете пользоваться такой терминологией и относить формулы или их имена которые Вы пишете на бумаге к
метатеории. Мне не очень понятно почему Вы не знаете, что предикат "z есть ZFC-формула " рекурсивен и представим в ZFC рекурсивной функцией. В нашем случае нету разницы между формулами метатеории и
формулами самой теории, поскольку эти объекты эквивалентны. Различие будет только тогда, если Вы определите формулы своей метатеории нерекурсивной процедурой. Там в конце Коэна есть приложение, где Вольпин
детально разъясняет процедуру погружения метатеории внутрь ZFC, что называется
арифметизацией метатеории. Высказывания (теоремы) при этом отождествляются с натуральными числами. Он даже и говорит о
теоремах-числах, чтобы подчеркнуть это.
Далее мне непонятно почему Вы решили, что мне
необходимо считать, что формулы обязательно образуют множество
Пусть это будет что угодно, класс например. Если Вы желаете работать только с метатеорией, то нет проблем. Строить множества с помощью счетного множества ZFC-формул ейной метатеории никому не запрещено. Эта процедура там также описана. Совершенно стандартная и древняя конструкция.
Другое дело, что в метатеории могут быть новые дополнительные предикаты, не выразимые в языке самой теории. Я такие предикаты очевидно нигде не использую.
Предикат
" замкнутая формула A выводима в ZFC" представим в
ZFC с помощью геделевского рекурсивного предиката
Pf(y,x) самой этой теории
ZFC
Далее, если Вы внимательно читали, то знаете, что Коэн доказывает эту обобщенную теорему о полноте именно в предположении, что множество формул есть обычное множество, в том смысле, что к этим Вашим метамножествам применимы все аксиомы ZFC кроме фундирования. Обратите также внимание, что эти геделевские модели
нестандартны, там почти все множества и отношение принадлежности не являются тем же, что и в обычной математике, это нечто совершенно другое. Стандартная модель была вперые построена именно Геделем, исходя из пустого множества, это его т.н. конструктивный универсум
L. Обратите внимание что этот универсум определен через счетное множество формул. То что я обозначаю через
Def[ZFC] это отличается от его конструкции только техническими деталями, связанными с тем, что мне нужен только счетный конструктивный универсум.
Def[ZFC] это просто некоторое счетное
подмножество класса
PRUV-класса всех множеств существование которых доказуемо в ZFC.
Ну я могу еще согласиться с тем, что не каждому математику очевидно, что
Def[ZFC] это именно счетное множество, а не счетный класс
, но доказательство этого факта, на самом не сложно, просто я его там не приводил, потому что оно длинное,
хотя и совершенно стандартное.
Но я могу избавить Вас от разбирательства с этим доказательством. На самом деле
использование мною этого злополучного множества
Def[ZFC] не играет никакой
важной роли. Я могу просто взять любое бесконечное
подмножество K в PRUV и
определить точно таким же приемом как и ранее,
новое дикое расселовское множество S## через это K тривиальным применением аксиомы выделения. Это новое множество тоже будет противоречивым. В этом случае как говориться крыть уже будет нечем. Я беру NGB вместо своей метатеории, а в ней класс
PRUV определен корректно и существует как подкласс универсального класса
V.