Модели теорий второго порядка

[epros]

У меня возникло некое ощущение непонимания того, что следует считать моделью теории, формализованной в исчислении предикатов второго порядка. Вот например, Дедекинд (вроде бы) доказал категоричность арифметики Пеано с аксиомой индукции второго порядка в так называемой "полной" семантике второго порядка. Это значит, что все модели этой теории изоморфны. Теперь я беру гипотезу континуума и формулирую её на языке исчисления предикатов второго порядка. Очевидно, что это возможно, причём без привлечения каких бы-то ни было дополнительных символов. Стало быть, она автоматически оказывается предложением в языке арифметики Пеано второго порядка. В её модели данное предложение оказывается либо истинным, либо ложным. В силу изоморфизма, гипотеза континуума должна оказаться либо истинной во ВСЕХ моделях арифметики второго порядка, либо ложной опять же во ВСЕХ её моделях. Правильно?

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

[Someone]

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

[epros]

Вот смотрите, что ответил на мой вопрос автор статьи про логику второго порядка в английской википедии:

Цитата:

CH is expressible in second-order logic via the sentence:

For all X, a, b, f, g, R such that X is an uncountable set, a and b are elements of X, f and g are functions from X to X, R is a linear order relation on X, and (X,a,b,f,g,R) is a complete ordered field: for every uncountable set Y there is a surjection from Y to X.

This is true in every countable model, and it is true in every uncountable model if CH is true and false in every uncountable model if CH is false. So it is a validity if CH is true.

Последнего предложения я не понимаю. По-моему, это какой-то fake. Как можно говорить об общезначимости (logical validity), при условии, что гипотеза континуума верна? Я ровно таким же образом могу заявить, что формула x+y=y+x общезначима "при условии коммутативности сложения". Бред какой-то... Нет, не понимаю я "семантики" второго порядка, в частности - понятия общезначимости.

[Xaositect]

Общезначимость - это истинность в любой модели. Для того, чтобы определить модель, в метатеории должна быть некоторая теория множеств. Так вот, если в метатеории верна гипотеза континуума, то в любой несчетной модели это утверждение будет выполняться (а в счетных выполняется автоматически), т.е. будет общезначимым. А если не верна, то не будет.

[epros]

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

...если в метатеории верна гипотеза континуума...

А если в метатеории нет ни соответствующей аксиомы, ни её отрицания (ровно так же, как обычно в метатеории нет ничего про коммутативность сложения)? Насколько я понимаю, в заявлении об отсутствии для логики второго порядка аналога теоремы полноты (которое выводится, как я понял, именно из Дедекиндовского доказательства категоричности арифметики второго порядка) должен быть какой-то глубокий смысл. Пока его не видно...

[Someone]

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

Общезначимость - это истинность в любой модели. Для того, чтобы определить модель, в метатеории должна быть некоторая теория множеств. Так вот, если в метатеории верна гипотеза континуума, то в любой несчетной модели это утверждение будет выполняться (а в счетных выполняется автоматически), т.е. будет общезначимым. А если не верна, то не будет.

Хм... Это, видимо, какая-то специфика теорий второго порядка? Потому что для теорий первого порядка эти утверждения неверны.

[Xaositect]

Someone в сообщении #467777 писал(а):

Это, видимо, какая-то специфика теорий второго порядка?

Да, в теории второго порядка можно выразить свойство "множество несчетно", "множество является моделью теории первого порядка T". Значит, можно и континуум с алефом сравнить.