Экстраполяция противоречивости

[Z1X]

Пусть имеется формальная теория $\mathrm{ZFC+\neg Con(ZFC)}$. Аксиома $\mathrm{\neg Con(ZFC)}$ означает, что в $\mathrm{ZFC}$ можно вывести некоторое утверждение и его отрицание. Но тогда и в $\mathrm{ZFC+\neg Con(ZFC)}$ можно вывести такое же противоречие, значит истинно $\mathrm{\neg Con(ZFC+\neg Con(ZFC))}$. Ведь все так?

[Someone]

А как в ZFC сформулировать ¬Con(ZFC)?

[Z1X]

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

[mihaild]

В моделях, где выполнено $\neg Cons(ZFC)$ выполнено и $\neg Cons(ZFC + X)$. Ну и что?

[Z1X]

mihaild в сообщении #1228536 писал(а):

В моделях, где выполнено $\neg Cons(ZFC)$ выполнено и $\neg Cons(ZFC + X)$. Ну и что?

В каких моделях? У $\mathrm{ZFC+\neg Con(ZFC)}$ нет моделей.

[Xaositect]

Z1X в сообщении #1228539 писал(а):

В каких моделях? У $\mathrm{ZFC+\neg Con(ZFC)}$ нет моделей.

Как это нет? Есть, просто доказательство противоречия будет нестандартным числом.

[mihaild]

Z1X в сообщении #1228539 писал(а):

В каких моделях? У $\mathrm{ZFC+\neg Con(ZFC)}$ нет моделей.

Есть (если у самой $ZFC$ есть модели).

[Someone]

Z1X в сообщении #1228466 писал(а):

Ну, предположим, вот как-то удалось выразить.

Ну почему же? Это очень интересный вопрос. Теория множеств ведь имеет дело с множествами, а не со своими формулами и доказательствами. Как тут выразить непротиворечивость?

[Z1X]

Xaositect в сообщении #1228546 писал(а):

Как это нет? Есть, просто доказательство противоречия будет нестандартным числом.

mihaild в сообщении #1228548 писал(а):

Есть (если у самой $ZFC$ есть модели).

Тогда в этой модели будет истинно $\mathrm{\neg Con(ZFC+\neg Con(ZFC))}$, а значит истинно утверждение об отсутствии моделей.

[Xaositect]

Z1X в сообщении #1228561 писал(а):

Тогда в этой модели будет истинно $\mathrm{\neg Con(ZFC+\neg Con(ZFC))}$, а значит истинно утверждение об отсутствии моделей.

То есть Вы в качестве метатеории тоже берете $ZFC + \neg\operatorname{Con}(ZFC)$?

[Z1X]

Xaositect в сообщении #1228562 писал(а):

То есть Вы в качестве метатеории тоже берете $ZFC + \neg\operatorname{Con}(ZFC)$?

А не все равно, что взять в качестве метатеории, если в теории существует вывод $\dfrac {\mathrm{\neg Con(ZFC)}}{\mathrm{\neg Con(ZFC+\neg Con(ZFC))}}}$?

[mihaild]

Z1X в сообщении #1228561 писал(а):

а значит истинно утверждение об отсутствии моделей

Ну да, в этой модели нету моделей $ZFC$. И что?

Возможно, вам будет полезно разобрать такую задачку.
Давайте поверим, что $ZF$ непротиворечива. Тогда у нее есть модель. Тогда по теореме Лёвенгейма-Скулема у нее есть счетная модель. В частности, все множества в этой модели не более чем счетные.
Но средствами $ZF$ доказывается существование счетного множества, несчетность множества всех подмножеств счетного множества и существование множества всех подмножеств данного множества - итого, средствами $ZF$ доказывается существование несчетного множества. Но в нашей модели все множества не более чем счетные. Как же так?

[Z1X]

mihaild, парадокс Сколема.

[mihaild]

Он самый. Вот как там "несчетность с точки зрения" модели - это что-то странное, так и "доказательства" в модели $ZFC + \neg Cons(ZFC)$ - тоже что-то странное.

[Xaositect]

Z1X в сообщении #1228564 писал(а):

А не все равно, что взять в качестве метатеории, если в теории существует вывод $\dfrac {\mathrm{\neg Con(ZFC)}}{\mathrm{\neg Con(ZFC+\neg Con(ZFC))}}$?

Но ведь вывод о существовании модели делается не в теории, а в метатеории.