Правило вывода Gen

[Sonic86]

1. Читал Мендельсона, увидел правило вывода Gen:
если $A$ - формула, то $A \vdash (\forall x)A$
Мне непонятно, как такая формула может быть правилом вывода, если я могу подобрать $A$ и значения переменных так, что получится ложный вывод. Например $A(x)=[2|x]$(2 делит $x$), $A$ задан на множестве целых чисел. Тогда полагая $x=2$ получаем, что посылка истинна, а вывод - нет. Даже представить себе не могу, что здесь не так.
На конечном множестве $M=(a_1,...,a_n)$ Gen выглядит вообще убийственно:
$A(x_j) \vdash A(x_1) \wedge ... \wedge A(x_n)$

2. Почему в узком исчислении предикатов не пользуются доказательством формул, аналогичных доказательству в алгебре высказываний. Т.е., например, если надо доказать $\vdash ((\exists xA(x)) \to C) \to (\forall y(A(y) \to C))$, то можно рассмотреть 2 случая: $C$ истинно и $C$ неистинно ($C$ - замкнутая формула, поэтому рассматриваем только 2 варианта). Подставляя в эту формулу, получим две формулы:
$\vdash 1 \to (\forall y 1)$ и $\vdash (\neg (\exists xA(x))) \to (\forall y( \neg A(y)))$
(я здесь пишу $C=1$, если при интерпретации и подстановке значений переменных $C$ истинно, иначе пишу $C=0$. $(\forall xA(x))=1$, если для всех $x$ $A(x)$ истинно)
Первая формула верна, вторая - тоже, как следствие из определения квантора $\exists$. Значит в общем формула тоже верна.
Если бы в формуле рассматривали не $C$, а $A(x)$, то было бы 4 варианта:
1. $(\forall x A(x))=1, A(x)=1, (\exists x A(x))=1$
2. $(\forall x A(x))=0, A(x)=1, (\exists x A(x))=1$
3. $(\forall x A(x))=0, A(x)=0, (\exists x A(x))=1$
4. $(\forall x A(x))=0, A(x)=0, (\exists x A(x))=0$
Их можно было бы подставлять в формулу и отдельно доказывать.
Сам я ответил так: не получится аксиоматизировать теорию + в общем виде алгоритм проверки истинности формулы сложен, особенно если рассматривать предикаты с $n$ переменными. Но этот метод хотя бы правомерен, то есть я же им могу пользоваться?

[Хорхе]

1. Насколько я помню, $x$ не должна входить в $A$.

[mkot]

Sonic86 в сообщении #351799 писал(а):

1. Читал Мендельсона, увидел правило вывода Gen:
если $A$ - формула, то $A \vdash (\forall x)A$
Мне непонятно, как такая формула может быть правилом вывода, если я могу подобрать $A$ и значения переменных так, что получится ложный вывод. Например $A(x)=[2|x]$(2 делит $x$), $A$ задан на множестве целых чисел. Тогда полагая $x=2$ получаем, что посылка истинна, а вывод - нет. Даже представить себе не могу, что здесь не так.
На конечном множестве $M=(a_1,...,a_n)$ Gen выглядит вообще убийственно:
$A(x_j) \vdash A(x_1) \wedge ... \wedge A(x_n)$

Давайте сначала поймём, что утверждает правило $\mathrm{Gen}$ на бытовом языке: Если некоторая формула $A(x)$ истинна при любых значениях $x$, то формула $\forall x \, A(x)$ также истинна. Вспомните в матанализе сколько раз доказываются теоремы следующим образом. Говорим, пусть $\varepsilon$ -- задано, потом показываем, что что-то верно, для этого эпсилон. А потом говорится, так как эпсилон произвольно, то это верно для любого эпсилон. Вот это и утверждается.
Теперь понятно, что вы делаете здесь не так?

-- Пн сен 13, 2010 14:09:29 --

Sonic86 в сообщении #351799 писал(а):

1. Читал Мендельсона, увидел правило вывода Gen:
если $A$ - формула, то $A \vdash (\forall x)A$
Мне непонятно, как такая формула может быть правилом вывода, если я могу подобрать $A$ и значения переменных так, что получится ложный вывод. Например $A(x)=[2|x]$(2 делит $x$), $A$ задан на множестве целых чисел. Тогда полагая $x=2$ получаем, что посылка истинна, а вывод - нет. Даже представить себе не могу, что здесь не так.
На конечном множестве $M=(a_1,...,a_n)$ Gen выглядит вообще убийственно:
$A(x_j) \vdash A(x_1) \wedge ... \wedge A(x_n)$

2. Почему в узком исчислении предикатов не пользуются доказательством формул, аналогичных доказательству в алгебре высказываний. Т.е., например, если надо доказать $\vdash ((\exists xA(x)) \to C) \to (\forall y(A(y) \to C))$, то можно рассмотреть 2 случая: $C$ истинно и $C$ неистинно ($C$ - замкнутая формула, поэтому рассматриваем только 2 варианта). Подставляя в эту формулу, получим две формулы:
$\vdash 1 \to (\forall y 1)$ и $\vdash (\neg (\exists xA(x))) \to (\forall y( \neg A(y)))$
(я здесь пишу $C=1$, если при интерпретации и подстановке значений переменных $C$ истинно, иначе пишу $C=0$. $(\forall xA(x))=1$, если для всех $x$ $A(x)$ истинно)
Первая формула верна, вторая - тоже, как следствие из определения квантора $\exists$. Значит в общем формула тоже верна.
Если бы в формуле рассматривали не $C$, а $A(x)$, то было бы 4 варианта:
1. $(\forall x A(x))=1, A(x)=1, (\exists x A(x))=1$
2. $(\forall x A(x))=0, A(x)=1, (\exists x A(x))=1$
3. $(\forall x A(x))=0, A(x)=0, (\exists x A(x))=1$
4. $(\forall x A(x))=0, A(x)=0, (\exists x A(x))=0$
Их можно было бы подставлять в формулу и отдельно доказывать.
Сам я ответил так: не получится аксиоматизировать теорию + в общем виде алгоритм проверки истинности формулы сложен, особенно если рассматривать предикаты с $n$ переменными. Но этот метод хотя бы правомерен, то есть я же им могу пользоваться?

Давайте я здесь тоже без сложных слов обойдусь. Что мы имеем для высказываний:
(1) Алгебра высказываний;
(2) Исчисление высказываний.
И в них принципиально разный подход. в алгебре мы придумываем значения переменных когда что-то доказываем про истинность или ложность, то есть оперируем значениями.
В исчислении высказываний мы имеем набор аксиом и правила вывода. И можем только с помощью них что-то делать, то есть здесь подход синтаксический, к смыслу самой формулы не апеллирующий.
Потом доказывается теорема о полноте, утверждающая, что как бы мы не доказывали всё равно одно и тоже получим.

С предикатами та же петрушка, есть:
(1) Исчисление предикатов;
(2) Теория моделей.
В первом случае мы также имеем только набор аксиом и правила вывода и работаем только с записями формул. Во втором случае мы придумываем модели, то есть носитель и интерпретируем символы сигнатуры. Также есть теорема о полноте.

Коротко: есть два подхода синтаксический и семантический, и они дают одинаковые результаты.

[Sonic86]

Хорхе писал(а):

1. Насколько я помню, $x$ не должна входить в $A$.

Я там посмотрел - такого исключения не заметил Если не входит, тогда да - проблем нет.

mkot писал(а):

Давайте сначала поймём, что утверждает правило $\mathrm{Gen}$ на бытовом языке: Если некоторая формула $A(x)$ истинна при любых значениях $x$, то формула $\forall x \, A(x)$ также истинна.

Ага! Я тоже думал, что может быть надо думать "при любых $x$". Но тогда будет проблема: либо нельзя в формулы ИП подставлять конкретные значения переменных и получать истинные формулы в ИВ, либо я тогда не понимаю как тогда в ИП изображаются предикаты. Предикат - это формула в ИП? Вроде бы в книге было написано, что $Gen$ применяется к любым формулам... Я еще посмотрю точнее и переспрошу, если не пойму.

mkot писал(а):

С предикатами та же петрушка, есть:
(1) Исчисление предикатов;
(2) Теория моделей.
В первом случае мы также имеем только набор аксиом и правила вывода и работаем только с записями формул. Во втором случае мы придумываем модели, то есть носитель и интерпретируем символы сигнатуры. Также есть теорема о полноте.

Коротко: есть два подхода синтаксический и семантический, и они дают одинаковые результаты.

Ага, ну ладно. Понял
Спасибо всем!

[mkot]

Sonic86 в сообщении #351905 писал(а):

Хорхе писал(а):

1. Насколько я помню, $x$ не должна входить в $A$.

Я там посмотрел - такого исключения не заметил Если не входит, тогда да - проблем нет.

Нет такого ограничения.

Sonic86 в сообщении #351905 писал(а):

Ага! Я тоже думал, что может быть надо думать "при любых $x$". Но тогда будет проблема: либо нельзя в формулы ИП подставлять конкретные значения переменных и получать истинные формулы в ИВ, либо я тогда не понимаю как тогда в ИП изображаются предикаты. Предикат - это формула в ИП? Вроде бы в книге было написано, что $Gen$ применяется к любым формулам... Я еще посмотрю точнее и переспрошу, если не пойму.

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

Про переменные. Не произвольные же формулы являются теоремами. А только, те которые выводятся из аксиом, согласно заданным правилам.
То есть вот возьмём аксиому (ну или умно: формулу полученную по первой схеме аксиом) $P(x) \to (P(x) \to P(x))$. Хоть заподставляйтесь вместо $x$ всё что угодно. И как угодно интерпретируйте $P$ всё одно истина получится.
А возьмёте формулу P(x) вы можете так придумать $x$ и $P$ что она будет и истинна и ложна. А ведь и правда, почему она должна быть истинной? Ведь мы её не вывели ниоткуда. (Конечно может так случиться что произвольно взятая формула будет истинной при любой интерпретации и любых значениях переменных, но тогда можно для неё и вывод будет построить.)
Про такие формулы и пишут $\vdash \varphi$ (то есть слева от значка ничего не ставят) и называют общезначимыми.
Но нам хочется большего, мы хотим ещё аксиом (например, порядка, теории групп и так далее) и понять что выводится из них. Если вам интересно, и вам не кажется что я вас только запутываю, то могу и про это рассказать.

(Оффтоп)

Каждый раз как открою Мендельсона такая грусть на меня находит, лучше уж Верещагин, Шень, там весело.

[Someone]

Тут есть такое соглашение: если формула $A$ содержит свободные переменные, то она интерпретируется так, будто по этим переменным стоят кванторы всеобщности. Поэтому правило $A\vdash(\forall x)A$ просто превращает неявный, подразумеваемый квантор в явно написанный.

-- Пн сен 13, 2010 20:03:33 --

Sonic86 в сообщении #351799 писал(а):

На конечном множестве $M=(a_1,...,a_n)$ Gen выглядит вообще убийственно:
$A(x_j) \vdash A(x_1) \wedge ... \wedge A(x_n)$

Здесь путаница. $a_1,a_2,\ldots,a_n$ - это константы, а $x_1,x_2,\ldots,x_n$ - переменные. В частности, $x_j$ никакого отношения к $a_j$ не имеет. Вместо $x_j$ может быть подставлена любая константа, в том числе, конечно, и $a_j$, но не только $a_j$.
Истинность формулы со свободными переменными означает, что при подстановке любых термов вместо свободных переменных получается истинное высказывание.

[Sonic86]

Someone
Спасибо! Мне понятно. Значит неявный квантор всеобщности.
Про $x_j$ напутал - там $a_j$ хотел написать.

mkot, спасибо, не запутываете, предикаты значит просто не выводятся сами по себе (из аксиом) + я там еще забыл отличие переменной от постоянной...
И значит в формулы вида $A \vdash B$ я не могу в существующие свободные переменные подставлять конкретные значения переменных... , ну в принципе тоже логично, если помнить об истинности посылок.
А вообще какие книжки по логике можете посоветовать. Я еще хотел Клини посмотреть, а там что-то мутновато мне показалось... или нет?

[mkot]

Цитата:

mkot, спасибо, не запутываете, предикаты значит просто не выводятся сами по себе (из аксиом) + я там еще забыл отличие переменной от постоянной...
И значит в формулы вида $A \vdash B$ я не могу в существующие свободные переменные подставлять конкретные значения переменных... , ну в принципе тоже логично, если помнить об истинности посылок.

Всё-таки я вас запутал. Нужно аккуратнее было отнестись.
Во-первых, запись $A \vdash B$ -- это не формула, это сокращение выражения "из $A$ следует $B$". Больше это ровным счётом ничего не значит. Подставлять в неё что-то тоже бессмысленно так как такая операция попросту не определена. (И вообще с ней нужно очень аккуратно обращаться.)
Но что-то мы можем в этом случае сказать. А именно. Пусть у нас собственно исчисление предикатов (то есть добавочных аксиом, как то: равенства, порядка, групп, и т. д. нет). Тогда с помощью Gen и MP мы из этих схем аксиом можем вывести какие-то формулы (ещё раз повторю -- синтаксически вывести, никакого смысла в символы переменных и сигнатуры не вкладывая). Такие формулы назовём выводимыми в исчислении предикатов. Обозначим $\vdash \varphi$. Так вот имеет место теорема корректности, что если формула выводима, то она будет и общезначима:
$\vdash \varphi \quad \Rightarrow \quad \models \varphi$.
(В обратную сторону пока умолчим.)

Вот теперь самое интересное что вы хотите и понять видимо.
Пусть у нас теперь есть ещё какие-то формулы из которых мы хотим что-то повывоить, их назовём тоже аксиомами.
Итак, пусть $\varphi$ -- формула.
Мы совершенно спокойно можем по правилу Gen записать что сказать
"из $\varphi$ следует $\forall x \, \varphi$.
Например, если была свободная переменная $x$, навешиваем на неё квантор. Но!!! никто не говорит, что в этом случае $\varphi$ логически влечёт $\forall x \, \varphi$. Хотя бы по той причине, что если переменная существенная, то вы даже определение не примените. Кстати, не надо воспринимать что "из $\varphi$ следует $\psi$" всегда есть
$\vdash \varphi \to \psi$. Теорема о дедукции как раз утверждает когда это имеет место. (Но "$\varphi$ логически влечёт $\psi$" эквивалентно $\models \varphi \to \psi$.)

А про ту трактовку Gen про которую я тут говорил: её можно воспринимать так:
если $\varphi$ выводима в исчислении предикатов, то $\forall x \,\phi$ также выводимо в исчислении предикатов.

[Sonic86]

Понятно, надо было серьезнее отнестись к курсу логики в универе. Мне почему-то представлялась теорема дедукции какой-то сверхочевидной вместе с правилом подстановки. Теперь вот вижу, что это не так. Надо все заново полностью перечитать и аккуратно обдумать.