Квантор всеобщности

[Qlin]

Считается, что навешивание по всем свободным переменным кванторов всеобщности даёт эквивалентную формулу:
$\forall x_0 \forall x_1 \forall x_2 \ldots \varphi \longleftrightarrow \varphi $
Для меня это странно и непонятно, потому что формула, содержащая свободные переменные, считается эквивалентной высказыванию.
Разберём конкретный пример:
$\forall x,y \ x=y \longleftrightarrow x=y $
Пусть модель содержит более одного элемента. Справа формула, истинность которой зависит от того, какие именно элементы предлагается взять в качестве $x$ и $y$. Формула слева не может быть истинной ни при каких обстоятельствах — это ложное высказывание. Каким образом они могут быть эквивалентны?

[george66]

Оно не даёт эквивалентную формулу, там более слабая вещь - равнодоказуемость. Например, мы можем принять аксиому
$x=x$
а можем с квантором
$\forall x(x=x)$
и это всё равно, потому что из первой формулы выводится вторая (применением кванторного правила). Вообще, доказать $\varphi(x)$ (без посылок) это всё равно что доказать $\forall x\varphi(x)$
Если значок "доказуемо" обозначить $\square$, то можно записать правильно
$\square(\varphi(x))\Leftrightarrow \square(\forall x\varphi(x))$

[Pphantom]

(george66)

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

(обычно пишут не $D$, а квадратик, но квадратик почему-то не набирается).

$\square$

[arseniiv]

Я видел как при определении значения формулы его иногда берут зависящим от значений всех возможных переменных (то есть оценка — это всегда функция $V\to\mathbb B$) — содержит ли она какую или нет, не замечая — и проделывают неявное $\forall$-замыкание для всех свободных, так что тогда и получается та эквивалентность просто по определению. Если же так не разбрасываться, останется только то, что уже написал george66.

[Qlin]

george66, из первой формулы выводится вторая применением кванторного правила. А как доказать в обратную сторону? Можно небольшую подсказку или намёк какой-нибудь?

[arseniiv]

А какая аксиоматика? Есть ли аксиома $(\forall x\varphi)\to\varphi[t/x]$?

-- Вс июн 16, 2019 23:02:14 --

Если «кванторное правило» было Gen или соотв. правило Бернайса.

[george66]

Обычно есть аксиома
$\forall x\varphi(x)\Rightarrow\varphi(t)$
где $t$ любой терм. Можно взять переменную $x$ в качестве $t$
$\forall x\varphi(x)\Rightarrow\varphi(x)$
Но вообще, есть разные аксиоматики.

[Someone]

Qlin в сообщении #1399549 писал(а):

Считается, что навешивание по всем свободным переменным кванторов всеобщности даёт эквивалентную формулу:

Довольно часто принимается соглашение «формула со свободными переменными интерпретируется так, будто на все свободные переменные "навешены" кванторы всеобщности». Такая интерпретация лично мне кажется естественной, так как если формула будет истинной при подстановке вместо свободных переменных любых объектов "мира", то она будет истинной и с кванторами всеобщности, и наоборот.