Почему обобщение определяется правилом вывода?

[epros]

Вопрос по разделу 4.2 "Аксиомы и правила вывода" части 2 "Языки и исчисления" Лекций по математической логике и теории алгоритмов, Н.К. Верещагин, А. Шень.

Почему правило обобщения $\varphi \vdash \forall \xi~\varphi$ определяется авторами именно как правило вывода? Даже правила Бернайса ими в конечном итоге было предложено сформулировать аксиомами. Что мешает обобщение также определить схемой аксиом $\varphi \to \forall \xi~\varphi$? Почему недостаточно одого правила modus ponens?

[george66]

Эта схема аксиом неверна. Пример такой "аксиомы"
$x<0\to\forall x(x<0)$
Это значит "если некоторое число $x$ меньше нуля, то все числа меньше нуля". В виде правила
$x<0\vdash\forall x(x<0)$
всё работает правильно, потому что означает "если мы можем доказать $x<0$, где про $x$ ничего не известно (это свободная переменная), то можно считать доказанным, что любой $x$ меньше нуля".

[gefest_md]

В учебнике встречаются и горизонтальная черта, и знак $\vdash$, которые понимаются по-разному. Горизонтальная черта означает, что есть два вывода и если существует верхний, то существует и нижний: если $\vdash C\to A(x)$, то $\vdash C\to\forall xA(x).$ Знак $\vdash$ это про один вывод.

[george66]

Честно говоря, не помню их обозначений.

[epros]

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

$x<0\to\forall x(x<0)$
Это значит "если некоторое число $x$ меньше нуля, то все числа меньше нуля". В виде правила
$x<0\vdash\forall x(x<0)$
всё работает правильно, потому что означает "если мы можем доказать $x<0$, где про $x$ ничего не известно (это свободная переменная), то можно считать доказанным, что любой $x$ меньше нуля".

Да, про "некоторое число" понятно. А откуда вообще берётся про "доказать $\varphi$, где про $x$ ничего не известно"? Как я понимаю, при наличии у $\varphi$ свободных переменных "доказывать" её вообще неправильно, потому что это не предложение языка.

-- Вс авг 27, 2017 14:56:02 --

gefest_md в сообщении #1243404 писал(а):

В учебнике встречаются и горизонтальная черта, и знак $\vdash$, которые понимаются по-разному. Горизонтальная черта означает, что есть два вывода и если существует верхний, то существует и нижний: если $\vdash C\to A(x)$, то $\vdash C\to\forall xA(x).$ Знак $\vdash$ это про один вывод.

Я правильно понимаю, что Вы говорите про разницу между мета-теоретическими утверждениями $(T \vdash A) \to (T \vdash B)$ и $T, A \vdash B$?
Т.е. именно первый вариант должен быть записан как

$$\frac{A}{B}?$$

[iifat]

Подозреваю, ответ примерно как на вопрос «почему modus ponens, а не modus tollens?»: автору так больше понравилось.

[gefest_md]

epros в сообщении #1243417 писал(а):

Я правильно понимаю, что Вы говорите про разницу между мета-теоретическими утверждениями $(T \vdash A) \to (T \vdash B)$ и $T, A \vdash B$?
Т.е. именно первый вариант должен быть записан как

$$\frac{A}{B}?$$

Да. Но последняя запись соответствует первому варианту без $T$.

[george66]

epros в сообщении #1243417 писал(а):

Да, про "некоторое число" понятно. А откуда вообще берётся про "доказать $\varphi$, где про $x$ ничего не известно"? Как я понимаю, при наличии у $\varphi$ свободных переменных "доказывать" её вообще неправильно, потому что это не предложение языка.

В том то и соль, что мы можем доказывать утверждения со свободными переменными. Например, если взять за аксиомы коммутативность, ассоциативность и дистрибутивность, мы можем вывести
$(x+1)^2=x^2+2\cdot x+1$
Поскольку про $x$ ничего не известно, мы заключаем, что
$\forall x\,((x+1)^2=x^2+2\cdot x+1)$
Свободная переменная -- это как бы "элемент, про который ничего не известно". Если мы смогли про него что-то доказать, оно должно быть верно для всех элементов.

[epros]

gefest_md в сообщении #1243419 писал(а):

Да. Но последняя запись соответствует первому варианту без $T$.

Как это без $T$? Разве речь в правиле вывода идёт об общезначимых $A$ и $B$? По-моему, речь о выводимости в рамках некой (произвольно выбранной) теории.

И, по-моему, разницы между первой и второй записью нет. Вторая запись говорит, что $B$ выводимо в теории, в которую добавлено $A$. А первая запись говорит, что $B$ выводимо в теории, если $A$ выводимо в этой теории (например, потому что было туда добавлено).

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

В том то и соль, что мы можем доказывать утверждения со свободными переменными

Как я понимаю, это означает, что мы на уровне синтаксиса признаём формулы со свободными переменными предложениями языка. Зачем нам тогда вообще нужно добавлять квантор всеобщности? Разве что для использования получившегося выражения как часть другой формулы...

Вот что я хочу сказать: Формула $\varphi \to \forall x~\varphi$ конечно же неверная, но и с соответствующим правилом что-то явно не так. В частности, в статье википедии про правила вывода правило Universal Generalization изложено несколько иначе (с ограничениями). А в статье конкретно про Universal Generalization даже приведены примеры некорректного применения данного правила, если пренебречь данными ограничениями.

[gefest_md]

Слева от знака $\vdash$ я пишу только формулы. Если эти формулы есть в первом варианте, тогда надо бы переписать их и в записи с горизонтальной чертой.
Но разница между вариантами существует:
Верно, что если $\vdash x=1$, то $\vdash\forall x(x=1)$ (в арифметике), по правилу обобщения.
Но неверно, что $x=1\vdash\forall x(x=1)$. Если это было бы верно, то можно было бы применить теорему о дедукции. Затем применяя правило обобщения, подстановку, МП и еще раз подстановку мы получили бы, что, например, $2=1.$

[george66]

epros в сообщении #1243427 писал(а):

Как я понимаю, это означает, что мы на уровне синтаксиса признаём формулы со свободными переменными предложениями языка. Зачем нам тогда вообще нужно добавлять квантор всеобщности? Разве что для использования получившегося выражения как часть другой формулы...

Конечно, мы на уровне синтаксиса признаём формулы со свободными переменными предложениями языка. Конечно, без квантора всеобщности мы не сможем записать формулу $\neg\forall x\varphi(x)$
Что касается строгой формулировки кванторных правил, там надо сначала определить подстановку и понять, как она работает. Запись $\varphi(x)$, строго говоря, неформальная. К сожалению, строгое изложение подстановки не просто трудно, а мучительно трудно, поэтому в подавляющем большинстве книг это объясняют "на пальцах".

[Slav-27]

epros в сообщении #1243392 писал(а):

Почему правило обобщения $\varphi \vdash \forall \xi~\varphi$ определяется авторами именно как правило вывода? Даже правила Бернайса ими в конечном итоге было предложено сформулировать аксиомами... Почему недостаточно одого правила modus ponens?

Почитал. Насколько я понял, допустимость этого "правила обобщения" следует из аксиом, правила modus ponens и правил Бернайса (поэтому "правило обобщения" можно было не упоминать вообще), и коль скоро последние сформулированы аксиомами, то одного правила modus ponens достаточно.

-- 27.08.2017, 22:08 --

А смысл самого правила, видимо, следующий: если что-то выводимо для произвольного $x$, то выводимо и для всех...

[epros]

gefest_md в сообщении #1243519 писал(а):

Слева от знака $\vdash$ я пишу только формулы. Если эти формулы есть в первом варианте, тогда надо бы переписать их и в записи с горизонтальной чертой.

Под $T$ и имеется в виду множество формул -. аксиом некой теории. Зачем их переписывать в варианте с чертой? Ясно же, что когда над чертой пишут $\varphi$, то имеют в виду формулу, выводимую из аксиом некой теории. Или Вы не согласны?

gefest_md в сообщении #1243519 писал(а):

Верно, что если $\vdash x=1$, то $\vdash\forall x(x=1)$ (в арифметике), по правилу обобщения.
Но неверно, что $x=1\vdash\forall x(x=1)$. Если это было бы верно, то можно было бы применить теорему о дедукции. Затем применяя правило обобщения, подстановку, МП и еще раз подстановку мы получили бы, что, например, $2=1.$

Понятно, что из $x=1 \vdash \forall x~(x=1)$ по теореме дедукции можно вывести то самое $\vdash x=1 \to \forall x~(x=1)$, которое неверно. Непонятно, почему это не работает для "если $\vdash x=1$, то $\vdash \forall x~(x=1)$". В чём суть различий между тем и другим? Я вижу разные формы записи одного и того же.

-- Вс авг 27, 2017 23:01:42 --

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

К сожалению, строгое изложение подстановки не просто трудно, а мучительно трудно, поэтому в подавляющем большинстве книг это объясняют "на пальцах".

Вроде, Верещагин и Шень довольно подробно объясняют, что такое "корректная" подстановка. Но почему-то при упоминании именно правила обобщения никакие подстановки не упоминаются.

Slav-27 в сообщении #1243536 писал(а):

Насколько я понял, допустимость этого "правила обобщения" следует из аксиом, правила modus ponens и правил Бернайса (поэтому "правило обобщения" можно было не упоминать вообще)

Если есть правила Бернайса (именно как правила), то правило обобщение из них, конечно, выводится.

Slav-27 в сообщении #1243536 писал(а):

и коль скоро последние сформулированы аксиомами, то одного правила modus ponens достаточно

Нет, там не так. Там сказано, что правила Бернайса можно заменить двумя аксиомами И правилом обобщения. Таким образом, у нас в системе помимо modus ponens остаётся только правило обобщения, остальное - аксиомы.

[arseniiv]

epros
Ну вот выразите правило обобщения через правила Бернайса и остальное, и все необходимые ограничения должны явиться сами собой.

gefest_md в сообщении #1243519 писал(а):

Но неверно, что $x=1\vdash\forall x(x=1)$. Если это было бы верно, то можно было бы применить теорему о дедукции.

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

(Оффтоп)

Как много специалистов по логике развелось, ужас. Я серьёзно.

-- Пн авг 28, 2017 00:20:34 --

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

-- Пн авг 28, 2017 00:27:02 --

epros в сообщении #1243548 писал(а):

Непонятно, почему это не работает для "если $\vdash x=1$, то $\vdash \forall x~(x=1)$". В чём суть различий между тем и другим? Я вижу разные формы записи одного и того же.

Видимо, в том, что это отдельные формулы, и если замкнуть $x = 1$, а потом повлечь из неё $\forall x(x = 1)$, получится $\forall x(x = 1)\to\forall x(x = 1)$, а если замкнуть $x = 1\to\forall x(x = 1)$, получающееся при неправильном выборе формулировки пары (вывод, теорема о дедукции), получится уже совсем другое $\forall x(x = 1\to\forall x(x = 1))$.

[george66]

Насколько я помню книгу Верещагина и Шеня (Верещагин подарил мне экземпляр), там всё изложено хорошо, кроме одного ляпа в главе про нестандартный анализ.