Математическая логика против теории множеств

[Sicker]

Сформулируем следующее логическое утверждение. Если мы можем доказать истинность А если А истинно, то можем доказать и ложность А если оно ложно. Действительно, если мы не можем доказать истинность А, значит оно не истинно, а значит ложно.
Теперь формулируем ситуацию применительно к теории множеств.
Утверждение А - какое-то число в натуральном ряду окрашено в красный цвет. Метод доказательства - прямой пересчет натуральных чисел.
Тогда если А истинно, то мы можем доказать, что такое число существует, просто дойдя до него за конечное количество шагов. А если оно ложно, мы ни за какое количество шагов не сможем убедиться, что оно ложно, ибо то красное число всегда может быть на шаг впереди.
Я утверждаю, что подобной ситуации нельзя добиться, не апеллируя к понятию бесконечности, а работая только с конечными множествами.

[Sender]

Sicker в сообщении #1360937 писал(а):

если мы не можем доказать истинность А, значит оно не истинно

А вдруг это только мы не можем, а Гриша с первой парты вполне себе может?

[Sicker]

Sender в сообщении #1360940 писал(а):

А вдруг это только мы не можем, а Гриша с первой парты вполне себе может?

По условию

Sender в сообщении #1360940 писал(а):

Мы можем доказать истинность А если А истинно

можем

[george66]

Если мы не можем доказать истинность $A$, это не значит, что мы можем доказать $\neg A$ (хотя оно истинно по условию). Контрпример вы сами привели (полуразрешимая формула, истинность которой можно проверить перебором, но как проверить её ложность?)

-- 14.12.2018, 05:31 --

Условие "из истинности следует доказуемость" предполагалось для формулы $A$. Для формулы $\neg A$ оно не предполагалось.

[mihaild]

Sicker в сообщении #1360937 писал(а):

Если мы можем доказать истинность А если А истинно, то можем доказать и ложность А если оно ложно

По-русски это записывается так: $(A \rightarrow \Box A) \rightarrow (\neg A \rightarrow \Box \neg A)$?
Это совсем не обяазательно верно.

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

Sicker в сообщении #1360937 писал(а):

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

Давайте возьмем скажем сигнатуру $=$ и пустую теорию (без аксиом). Возьмем одноэлементную модель этой теории. Рассмотрим утверждение $\exists x \exists y: x \neq y$. Оно ложно (в этой модели). Если оно истинно (в этой модели), то мы можем его доказать. Но оно ложно, и доказать его ложность мы не можем (потому что у этой теории есть модели, в которых это утверждение истинно). Никакая бесконечность тут не нужна.

[Sicker]

george66 в сообщении #1361229 писал(а):

Если мы не можем доказать истинность $A$, это не значит, что мы можем доказать $\neg A$ (хотя оно истинно по условию). Контрпример вы сами привели (полуразрешимая формула, истинность которой можно проверить перебором, но как проверить её ложность?)

Там используется понятие бесконечности. Вот если мы у нас была верхняя граница $n$ для числа переборов, тогда бы все было норм.

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

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

Вообще не понял, можно поподробнее?

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

Давайте возьмем скажем сигнатуру $=$ и пустую теорию (без аксиом). Возьмем одноэлементную модель этой теории. Рассмотрим утверждение $\exists x \exists y: x \neq y$. Оно ложно (в этой модели). Если оно истинно (в этой модели), то мы можем его доказать. Но оно ложно, и доказать его ложность мы не можем (потому что у этой теории есть модели, в которых это утверждение истинно).

Если мы рассматриваем одну модель, то и истинность определяем в этой модели, другие нас не интересуют. Зачем рассматривать другие?

[mihaild]

Sicker в сообщении #1361236 писал(а):

Вообще не понял, можно поподробнее?

Да, конечно. Верещагин, Шень "Языки и исчисления", параграф 3.1.

Sicker в сообщении #1361236 писал(а):

Зачем рассматривать другие?

Потому что выводимость в теории не зависит от того, какую модель мы рассматриваем.