Специфические тавтологии логики второго порядка

[kernel1983]

Интересно, где можно найти тавтологии, характерные для логики предикатов второго порядка? Я пока нашёл только одну (на этом форуме). Эта формула имеет вид $\forall P ( \exists x P(x) \vee \overline{ \exists x P(x)})$.

[arseniiv]

Подобных этой можно нагенерировать кучу. Берём тавтологию первого порядка, в которой случайно попались функциональные/предикатные символы: $\forall x\forall y.P(x,y)\to\forall x.P(x,x)$. Добавляем кванторы по ним, переосмыслив их как переменные: $\forall P(\forall x\forall y.P(x,y)\to\forall x.P(x,x))$. Тавтология второго порядка готова, приятного аппетита!

Но это только по поводу этой.

[kernel1983]

arseniiv, спасибо.
Ну, значит, берём любую тавтологию логики предикатов первого порядка и навешиваем кванторы (любые?) по предикатным переменным?
А что-нибудь есть такое, где тавтологии первого порядка не участвуют?

[arseniiv]

Определённо не скажу. Здесь я просто взял, что плохо лежало.

kernel1983 в сообщении #1120601 писал(а):

Ну, значит, берём любую тавтологию логики предикатов первого порядка и навешиваем кванторы (любые?) по предикатным переменным?

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

[kernel1983]

arseniiv в сообщении #1120604 писал(а):

И можно, конечно, навешивать кванторы по переменным, которые свободно не входят

А какой в этом смысл?

[arseniiv]

Кроме того, что получится другая формула, никакого, вот именно.