Ошибка Timothy Y. Chow

[xyzxyz]

В любой нестандартной модели ZFC, имеется нестандартная модель Nm(PA) арифметики Пеано PA, а в ней содержится ее обычная стандартная модель
Sm(PA) (Sm(PA) называется стандартным сечением нестандартной модели Nm(PA)). Возьмите коды доказательств в Sm(PA) и все они будут конечны.

[AGu]

Пусть $\mathcal M$ — нестандартная модель ZFC, $\mathcal N\subset\mathcal M$ — нестандартная модель PA, $N\subset\mathcal N$ — стандартная модель PA («стандартное сечение» $\mathcal N$).
Пусть $\varphi(x)$ — арифметическая формализация утверждения о том, что $x$ является кодом вывода противоречия из аксиом ZFC.
В рассматриваемой ситуации мы имеем ${\rm ZFC}\vdash(\exists\,x)\,\varphi(x)$.
Мне кажется понятным, что тогда существует элемент $\nu\in\mathcal N$ со свойством $\mathcal N\vDash\varphi(\nu)$.
Но мне непонятно, почему существует элемент $n\in N$ со свойством $N\vDash\varphi(n)$.
Это было бы так, если бы мы имели ${\rm PA}\vdash(\exists\,x)\,\varphi(x)$, но мы имеем всего лишь ${\rm ZFC}\vdash(\exists\,x)\,\varphi(x)$.

[xyzxyz]

1.Пусть ZFC$SM$ это релятивизация ZFC к ее некоторой стандартной модели $SM$. Пусть $\varphi(x,SM)$ — арифметическая формализация утверждения о том, что $x$ является кодом вывода противоречия из аксиом ZFCSM.
Если Вы хотите показать, что такой модели не существует, то нужно показать, что ${\rm ZFC$SM$}\vdash(\exists\,x)\,\varphi(x,SM)$.
2.Пусть ZFCNM это релятивизация ZFC к ее некоторой нестандартной модели $NM$. Пусть $\varphi(x,NM)$ — арифметическая формализация утверждения о том, что $x$ является кодом вывода противоречия из аксиом ZFCNM.Если Вы хотите показать, что такой модели не существует, то разумеется нужно показать, что ${\rm ZFC$NM$}\vdash(\exists\,x\in N)\,\varphi(x,NM)$. Таким образом нет большой разницы между случаями 1 и 2 и ограничение только стандартными моделями, вопреки замечанию Chow, никакой принципиальной роли не имеет.
PS. Разумеется, что автор топика на FOM, ничего не доказал даже для первого случая, а только предложил некую общую схему возможного доказательства, отсутствия у ZFC некоторых классов моделей.

[AGu]

xyzxyz в сообщении #729128 писал(а):

Пусть ZFC$SM$ это релятивизация ZFC к ее некоторой стандартной модели $SM$.

Хмм... Не могу понять. Какую сигнатуру имеет теория ZFC$SM$? Теоретико-множественную с добавленной константой $SM$? Или — еще вариант — с добавленным классом (точнее, одноместным предикатным символом) $SM$? (Больше ничего более-менее подходящего в голову не приходит.)

xyzxyz в сообщении #729128 писал(а):

Пусть $\varphi(x,SM)$ — арифметическая формализация утверждения о том, что $x$ является кодом вывода противоречия из аксиом ZFCSM.

Если у нас в сигнатуре появился новый символ $SM$, то как формула $\varphi(x,SM)$ может быть арифметической? Чтобы она была арифметической, символ $SM$ должен допускать арифметическую элиминацию (определение в арифметических терминах), но я не вижу такой возможности.

[xyzxyz]

Формула $\varphi(x,T)$ будет арифметической для любой рекурсивно аксиоматизируемой теории T первого порядка. От сигнатуры T это никаким боком не зависит. Пусть Con(ZFC;SM) обозначает предложение, которое утверждает, что множество SM есть стандартная модель для ZFC. Единственное необходимое условие для SM так это то, что предложение Con(ZFC;SM) должно быть выразимо в ZFC.

[AGu]

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

Итак:

xyzxyz в сообщении #728371 писал(а):

Chow wrote
"In order to deduce "ZFC is inconsistent" from "ZFC |- ~con(ZFC)" one needs something more than the consistency of ZFC, e.g., that ZFC has an omega-model (i.e., a model in which the integers are the standard integers)."
ничего такого something more конечно не требуется

Если я правильно интерпретировал Ваше сообщение, Вы утверждаете, что (вопреки высказыванию Chow) из ${\rm ZFC}\vdash \neg {\rm con}({\rm ZFC})$ все же можно (и по всей видимости, легко) вывести противоречивость ZFC.
Я тут не ошибся?
Тогда хотелось бы увидеть этот вывод — на современном уровне строгости и по возможности четко, без недосказанностей и неопределенных нетрадиционных обозначений.

[xyzxyz]

А что Вы подразумеваете под этим обозначением $ \neg {\rm con}({\rm ZFC})$? Отсутствие любой модели у ZFC или арифмктическое утверждение о ее противоречивости.
Пока я утверждаю, что первая теорема этого автора верна, но ее доказательство может быть проведено только на языке второго порядка. А вторая его теорема не верна, поскольку теорема Геделя говорит о недоказуемости непротиворечивости средствами языка первого порядка.

[AGu]

xyzxyz в сообщении #731179 писал(а):

А что Вы подразумеваете под этим обозначением $ \neg {\rm con}({\rm ZFC})$? Отсутствие любой модели у ZFC или арифмктическое утверждение о ее противоречивости.

У нас такой контекст:

Finnur Larusson на FOM писал(а):

Let con(ZFC) be a sentence in ZFC asserting that ZFC has a model.

Впрочем, по теореме о полноте особой разницы, вроде, нет (в рамках ZFC). Или тут есть какая-то тонкость?

[xyzxyz]

Тонкость в том, что такое понятие как произвольная модель ZFC, нельзя выразить на языке ZFC.

[AGu]

xyzxyz в сообщении #731191 писал(а):

Тонкость в том, что такое понятие как произвольная модель ZFC, нельзя выразить на языке ZFC.

Видимо, я опять не понимаю, о чем сейчас идет речь. Мне казалось, что фраза «$\langle M,\varepsilon\rangle$ является моделью ZFC» — заурядное утверждение (про $M$ и $\varepsilon$), вполне себе выразимое. Есть ведь такие понятия, как алгебраическая система, формула, аксиома, означивание переменных, истинность формулы в системе и т.д. и т.п. — все определяется и все формализуется на языке теории множеств (как в метатеории, так и в теории).

Как бы то ни было, если по каким-то причинам следует считать ${\rm con}({\rm ZFC})$ именно утверждением о непротиворечивости ZFC — нет проблем, давайте так считать.

[xyzxyz]

1.Фраза «$\langle M,\varepsilon\rangle$ является моделью ZFC» — заурядное утверждение (про $M$ и $\varepsilon$),
только в том случае, если имеется явное доказательство в ZFC утверждения:$\langle M,\varepsilon\rangle$ является моделью ZFC.
2.истинность формулы W в модели (системе) $\langle M,\varepsilon\rangle$ означает, что в ZFC выводима релятивизация W[M] этой формулы на M, т.е. ZFC|- W[M]. Таким образом, истинность формулы невозможно определить на языке первого порядка.

Автор топика пишет:
Claim 1. S is consistent.

Proof. Assume S is inconsistent, that is, has no model. This means
that there is no model of ZFC in which con(ZFC) is true,
Предложение: 'This means
that there is no model of ZFC in which con(ZFC) is true,'
в силу вышесказанного, можно формализовать, только на языке второго порядка, но не в ZFC.
Из его "there is no model of ZFC in which con(ZFC) is true," следует, что
~con(ZFC) истинно в любой модели ZFC, а значит и доказуемо в ZFC, что противоречит исходному предположению: con(ZFC).
Таким образом его Claim 1. верна, но это метатеорема, доказанная на языке второго порядка, а не в ZFC. Соответственно никакого противоречия с теоремой Геделя там на самом деле нет.

[AGu]

xyzxyz в сообщении #731405 писал(а):

1.Фраза «$\langle M,\varepsilon\rangle$ является моделью ZFC» — заурядное утверждение (про $M$ и $\varepsilon$),
только в том случае, если имеется явное доказательство в ZFC утверждения:$\langle M,\varepsilon\rangle$ является моделью ZFC.

Мне это заявление кажется весьма странным. (Вероятно, мы с Вами расходимся в каких-то неявных предположениях.) Фраза «$\langle M,\varepsilon\rangle$ является моделью ZFC» записывается (теоретико-множественной) формулой со свободными переменными $M$ и $\varepsilon$ в строгом соответствии с (теоретико-множественными) определениями таких понятий, как теория, алгебраическая система, формула, истинность формулы в системе и т.п. Для того, чтобы какое-либо утверждение было выразимым (на языке теории множеств), совершенно не нужно, чтобы это выражение было доказуемым (в теории множеств), правда ведь? В рамках метатеории множеств имеется классическое понятие модели теории, и нет ровным счетом никаких препятствий к тому, чтобы записать соответствующее определение на языке метатеории множеств. То же самое относится и к теории. Мы просто осуществляем «сдвиг платформ»: то, что было «метатеорией», становится «теорией», а бывшая «теория» превращается в «объект теории» — множество, допустимое значение терма. (Это классика. Редко разжевываемая в современных учебниках, но классика.)

xyzxyz в сообщении #731405 писал(а):

2.истинность формулы W в модели (системе) $\langle M,\varepsilon\rangle$ означает, что в ZFC выводима релятивизация W[M] этой формулы на M, т.е. ZFC|- W[M].

Нет, это не наш случай. (Возможно, в этом и заключается источник нашего взаимного недопонимания.) Сейчас речь идет вовсе не о так называемых внутренних моделях (обычно являющихся собственными классами и типичных для разного рода доказательств относительной совместности в рамках теории множеств), а о самых обычных моделях (являющихся множествами в метатеории и типичных для классической теории моделей). В этом случае истинность предложения $W$ в системе $\langle M,\varepsilon\rangle$, обычно записываемая в виде $\langle M,\varepsilon\rangle\vDash W$, выражается некоторой (вполне конкретной) формулой $\tau(M,\varepsilon,W)$ с тремя свободными переменными и представляет собой формализацию заурядного утверждения о трех множествах — $M$, $\varepsilon$ и $W$. Здесь $\tau$ и $W$ — формулы, но из разных теорий: $\tau$ — формула метатеории, а $W$ — формула теории, олицетворяемая переменной в формуле $\tau$ из метатеории. (Это, опять-таки, классика.)

xyzxyz в сообщении #731405 писал(а):

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

В рассматриваемом нами случае — возможно. Согласно теореме Тарского истинность действительно неформализуема, но там речь идет об истинности во внутренней модели-классе (применительно к теории множеств — в классе $\mathbb V$ всех множеств). У нас же модели — самые обычные, классические. Истинность в такой модели — обычное утверждение, прекрасно формализуемое.

[xyzxyz]

Нет проблем. Чтобы у нас не было разногласий в определениях, Вы можете считать, что рассматриваются только внутренние модели. Другие модели меня не интересуют. Итак пусть Соn(ZFC;StM) это предложение в ZFC утверждающее, что у ZFC существует некоторая внутренняя стандартная модель StM.

[AGu]

xyzxyz в сообщении #731672 писал(а):

можете считать, что рассматриваются только внутренние модели.

Тогда в данной теме это оффтопик, ибо участники цитируемой Вами дискуссии на FOM вне всяких сомнений (по умолчанию) вели разговор в рамках классического контекста с его классическими моделями.

xyzxyz в сообщении #731672 писал(а):

Другие модели меня не интересуют.

Как Вам будет угодно, топискстартер тут Вы, можете открыть новую тему (или подтему), а текущую тему лично я считаю исчерпанной.

[xyzxyz]

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