Кванторы и пропозициональные операции

[arseniiv]

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

Честное слово, именно в этом суть дела и именно это отражают правила вывода для квантора $\forall$ в исчислении предикатов. "Семантически" легче объяснить нельзя.

Если бы я был kernel1983 в том смысле, в котором я его сейчас представляю, меня бы это только запутало. Будем надеяться, что моя модель неверна.

[george66]

К сожалению, вопрос (семантика кванторов) действительно трудный.

[arseniiv]

Ну не знаю, когда я в первый раз читал про интерпретацию языка первого порядка, мне всё показалось очевидным (почти: сначала я не разобрался в механизме оценок, а через какое-то время переизобрёл его, а потом перечитал соответствующее место в какой-то книге и удивился), и даже без формального понимания интерпретации «коммутирование» $\forall$ и $\wedge$, насколько помню, мне казалось довольно естественным.

[Xaositect]

Как по мне, нет никакого сложного вопроса. Определение истинности по Тарскому - это просто перенос структуры рассматриваемой формулы в метатеорию. Соответственно, любое доказательство общезначимости просто апеллирует к аналогичному свойству в метатеории.
Например, коммутативность конъюнкции, если мы хотим доказывать ее через семантику, упирается в коммутативность связки "и" в метатеории.
Абсолютно точно так же и дистрибутивность кванторов потребует той же дистрибутивности в метатеории.

[george66]

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

Как по мне, нет никакого сложного вопроса. Определение истинности по Тарскому - это просто перенос структуры рассматриваемой формулы в метатеорию. Соответственно, любое доказательство общезначимости просто апеллирует к аналогичному свойству в метатеории.

Да-да, именно это и смущает kernel1983, почитайте его первое сообщение.
Кстати, почему квантор $\exists$ коммутирует с дизъюнкцией? А потому что он тоже действует так $\exists_f\colon P(X)\to P(Y)$
$\exists_f(A)=f[A]=\{y\in Y\mid \exists x\in X (f(x)=y \wedge x\in A)\}$
(по подмножеству $A\subseteq X$ выдаёт его образ), но присобачен слева, а не справа
$\exists_f(A)\subseteq B$ если и только если $A\subseteq f^{-1}(B)$
(образ $A$ включён в $B$ если и только если $A$ включено в прообраз $B$)

-- 12.04.2017, 17:25 --

[arseniiv]

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

Да-да, именно это и смущает kernel1983, почитайте его первое сообщение.

Там, по-моему, скорее упоминается замкнутый круг, которого нет, если метатеорию не отождествлять с теорией.

[george66]

Кванторные правила в исчислении предикатов примерно так и выглядят
$B\vdash A(x)$ если и только если $B\vdash\forall x A(x)$
$\exists x A(x)\vdash B$ если и только если $A(x)\vdash B$
Тут ещё надо объяснять, конечно (где тут взятие прообраза неявное), но суть дела именно в соответствии Галуа.