Логика и теория множеств

[arseniiv]

(Оффтоп)

Мда.

[deep blue]

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

Можно, например, рассмотреть метатеории $ZFC + \operatorname{Con}(ZFC)$ и $ZFC + \neg \operatorname{Con}(ZFC)$ и что они говорят о выполнимости $ZFC$.

Правильно ли я понимаю, что метатеория $ZFC + \neg \operatorname{Con}(ZFC)$ заведомо противоречива так как постулирует противоречивость части своих аксиом? Если так, то наверное не имеет значения, что она говорит.

[Xaositect]

deep blue в сообщении #1081016 писал(а):

Правильно ли я понимаю, что метатеория $ZFC + \neg \operatorname{Con}(ZFC)$ заведомо противоречива так как постулирует противоречивость части своих аксиом?

Нет, тут все более хитро. $\operatorname{Con}(ZFC)$ - это утверждение об отсутствии доказательства противоречия. Доказательство при этом как-то представлено в метатеории, например, как строка символов, т.е. конечная последовательность элементов некоторого множества - алфавита. Конечная последовательность - это функция из некотрого начального отрезка натуральных чисел в алфавит. Так вот, проблема состоит в том, что $ZFC + \neg \operatorname{Con}(ZFC)$ обязана содержать нестандартные натуральные числа, то есть такие натуральные числа $z$, для которых справедливы все утверждения $z > 0$, $z > 1$, $z > 2$ и т.д. Эти нестандартные числа позволяют образовывать нестандартные доказательства, которые с точки зрения $ZFC + \neg \operatorname{Con}(ZFC)$ являются доказательствами, а с точки зрения здравого смысла не являются.

[Unx]

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

Обычно же в качестве метатеории выступает неформальная теория множеств

Наивная теория - это в строгом смысле вовсе не теория. В ней нет аксиом и правил вывода. Но вроде бы есть изначальное и единственное понимание того, какие выражения являются истинными, а какие ложными... К примеру выражение $\{ \varnothing \}=\varnothing$ мы воспринимаем как ложное. Выражение $\forall X \ \varnothing \subseteq X$ однозначно понимается как истинное (кстати его можно и "доказать", пользуясь теми же интуитивными рассуждениями). Так получается, что мы уже имеем изначально возможность интерпретировать формулы наивной теории, причем единственным образом?

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

Для того, чтобы определить семантические понятия, напр. модель теории, в метатеории должна быть какая-то теория множеств.

Если она наивная, то мы уже имеем некоторую семантику. Получается так?

[Xaositect]

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

Unx в сообщении #1083986 писал(а):

Но вроде бы есть изначальное и единственное понимание того, какие выражения являются истинными, а какие ложными... К примеру выражение $\{ \varnothing \}=\varnothing$ мы воспринимаем как ложное.

Эта ошибка часто втречается у новичков (тут на форуме много примеров), так что я бы не сказал, что это интуиция, это именно что надо доказывать себе, с учетом определения равенства множеств и пустого множества. Так что правила и аксиомы есть, они просто не записаны формально.

[Unx]

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

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

Я попробую доказать, а вы мне подскажете. Хорошо?
$(\{ \varnothing \}=\varnothing) \Leftrightarrow ((\{ \varnothing \} \subseteq \varnothing) \land (\{ \varnothing \} \supseteq \varnothing))$
Первая сложность: а что обозначает символ конъюнкции? В каком смысле он здесь используется? Если это бинарная логическая операция (заданная таблицей), то тогда пришлось бы вводить операции еще раньше понятия равенства множеств. Если это логическая связка в том виде, в каком она используется в исчислении предикатов, то мы вообще не имеем представления какие формулы считать истинными, а какие - ложными.

Кроме того $(\{ \varnothing \} \subseteq \varnothing) \Leftrightarrow (\forall x \ x \in \{ \varnothing \} \Rightarrow x \in \varnothing) $, и вторая сложность: что обозначает символ $\Rightarrow$ ? Если это тот же символ, который используется в исчислении предикатов, то единственное, что можно требовать - это вывод с помощью правила modus ponens. Я не представляю себе такой вывод для данной задачи.

-- 20.12.2015, 19:34 --

Уточню по поводу эквиваленции. $A \Leftrightarrow B$ можно в любом случае понимать как сокращение записи $(A \Rightarrow B) \land (B \Rightarrow A)$.

[Xaositect]

Мы же говорим о неформальной (наивной) теории? Тогда конъюнкция - это сокращение для связки "и" из естественного языка, а $\forall x (P(x) \rightarrow Q(x))$ - это обозначение для конструкции "для любого $x$, для которого выполняется $P$, выполняется и $Q$". И у нас есть методы, как эту конъюнкцию и это следование доказывать - для доказательства конъюнкции нужно доказать обе части, а для доказательства следования надо предположить $P$ и доказать $Q$. Мы это со школы знаем.

Unx в сообщении #1084020 писал(а):

Если это бинарная логическая операция (заданная таблицей), то тогда пришлось бы вводить операции еще раньше понятия равенства множеств.

Если хочется более строго определить правила, то можно сделать и так. Никакой проблемы тут нет, потому что нам не нужны операции, нам нужны операции над истинностными значениями $\mathrm{F}, \mathrm{T}$. Тут все значительно проще и никаких множеств не надо. Вот свободные переменные и кванторы - это другое дело.

А если надо делать все совсем строго, то надо вводить метатеорию и строго определять истинность и доказательство. Но все равно в конечном итоге последняя метатеория это неформальная математика.

[Unx]

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

Но все равно в конечном итоге последняя метатеория это неформальная математика.

Я как-то тоже подумал об этом.