Правило Бернайса

[kernel1983]

При построении исчисления предикатов используется такое правила вывода, как правило Бернайса: $F \to G(x) \vdash F \to \forall x G(x)$, где $G(x)$ содержит свободное вхождение $x$, а $F$ не содержит. Точнее, это одно из правил Бернайса. Если, например, вместо $F$ взять высказывание $A$ - "Двенадцать делится на шесть" (истинное), а вместо $G(x)$ взять предикат $P(x)$ - "$x$ делится на три", заданный на множестве натуральных чисел. Пусть $x=3$. Тогда высказывание $A \to P(3)$ истинно, а высказывание $A \to \forall x P(x)$ ложно. Значит, высказывание $(A \to P(3)) \to (A \to \forall x P(x))$ ложно. Значит, правило Бернайса не корректно? В чём моя ошибка?

[Someone]

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

В чём моя ошибка?

В том, что в правиле написано $G(x)$, а у Вас — $P(3)$.

Вообще, обычно формулы со свободными переменными интерпретируются так, как будто по всем свободным переменным стоят кванторы всеобщности.

[arseniiv]

Это правило Бернайса формализует рассуждение вида «если мы вывели из $F$, что некое $G(x)$ верно для свежего произвольного $x$, который мы ввели вот только что, то значит из $F$ следует $\forall x. G(x)$». Прозрачнее всего такие выводы выглядят в естественном выводе (aka натуральный вывод, натуральная дедукция, natural deduction), но так как там требуется рисовать деревья*, обычно для базовых курсов матлогики используют гильбертовский формализм.

* По крайней мере поначалу для поняности — а потом это всё можно сократить в линейную запись, перейдя к подходящей теории типов.

[kernel1983]

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

Это правило Бернайса формализует рассуждение вида «если мы вывели из $F$, что некое $G(x)$ верно для свежего произвольного $x$, который мы ввели вот только что, то значит из $F$ следует $\forall x. G(x)$».

Это другое: если $F \vdash G(x)$, то $ F \vdash \forall x G(x)$. Уже метатеорема, а не правило вывода.

[arseniiv]

Ну пара фиксов и будет правило, метатеорему о дедукции-то никто у нас не отнял. И натуральный вывод как раз немного освобождает от такого. Ведь импликация это и есть интернализация выводимости, насколько это разумно в том или ином исчислении, так что когда метатеорема о дедукции не особо выполняется, мы делаем что-то нехорошее с исчислением. (И например все ограничения на эту метатеорему в исчислении предикатов относятся к отсечению нездоровых манипуляций переменными. Часто её потому для простоты ослабляют так, что она работает только для замкнутых формул, но можно сильнее.)