Как доказать общезначимое высказывание с помощью исчисления

[arseniiv]

Kosat в сообщении #1009852 писал(а):

идёт рука об руку с некоторой невнимательностью

Есть такое иногда.

Мне сообщили в ЛС, что я неправильно прочитал «1б» — мне показалось, это число шестнадцать. Вот теперь посмотрел в этом месте и понимаю получше, хотя всё равно до конца ещё не понимаю — про штрих и про какие-то отличия именно в этом месте. В случае вывода $\Gamma,A\vdash B$, состоящего из одной формулы $B$, ничего нового исчисление предикатов не даёт — всё так же $B$ либо аксиома, либо входит в $\Gamma$, либо это $A$. Добавление новых аксиом и правил(а) вывода никак на этом случае не сказывается.

(Опять не знаю, известно ли уже вам следующее.) В случае исчисления предикатов теорема о дедукции уже, кстати не применима для любых формул (см., напр., Верещагин, Шень. Языки и исчисления §4.4 Выводы в исчислении предикатов). Работает, например, с такой дополнительной посылкой: если все $\Gamma,A$ — замкнутые, то $\Gamma,A\vdash B\Leftrightarrow \Gamma\vdash A\to B$. Кстати, почитайте доказательство оттуда — вряд ли я лучше напишу. (Там упоминаются правила Бернайса. Если у вас используется правило обобщения $A\vdash\forall x.\;A$ (и дополнительные аксиомы, соответственно, другого вида), придётся всё это добро вывести (только аксимы — правило выводится в §4.2).)

(Оффтоп)

Kosat в сообщении #1009852 писал(а):

Ваш быстрый ум

Kosat в сообщении #1009852 писал(а):

Уверен, это один из тех вопросов, которые легко решит человек, владеющий таинством логических формул.

Да куда уж «владеющий таинством». Не переоценивайте людей, они от этого портятся. Я вам и помочь-то смог в прошлый раз по чистой случайности.

[Kosat]

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

Мне сообщили в ЛС, что я неправильно прочитал «1б» — мне показалось, это число шестнадцать. Вот теперь посмотрел в этом месте и понимаю получше, хотя всё равно до конца ещё не понимаю — про штрих и про какие-то отличия именно в этом месте. В случае вывода $\Gamma,A\vdash B$, состоящего из одной формулы $B$, ничего нового исчисление предикатов не даёт — всё так же $B$ либо аксиома, либо входит в $\Gamma$, либо это $A$. Добавление новых аксиом и правил(а) вывода никак на этом случае не сказывается.

$B$ может быть результатом применения одного из правил Бернайса. Это и есть моей проблемой.

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

(Опять не знаю, известно ли уже вам следующее.) В случае исчисления предикатов теорема о дедукции уже, кстати не применима для любых формул (см., напр., Верещагин, Шень. Языки и исчисления §4.4 Выводы в исчислении предикатов). Работает, например, с такой дополнительной посылкой: если все $\Gamma,A$ — замкнутые, то $\Gamma,A\vdash B\Leftrightarrow \Gamma\vdash A\to B$.

По ссылке написано, что достаточна только замкнутость $A$. В вашей книге непонятно, как используется замкнутость остального. В примерах исходных данных моего задания на замкнутость этих сущностей, похоже, вообще не обращается внимание.
UPDATE:
По ссылке написано, что нужна замкнутость всего: $\Gamma,A$. Я не дочитал про «теорию». Но что делать с примерами исходных данных моего задания с ошибками по замкнутости этих сущностей, все равно не понятно.

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

Кстати, почитайте доказательство оттуда — вряд ли я лучше напишу. (Там упоминаются правила Бернайса. Если у вас используется правило обобщения $A\vdash\forall x.\;A$ (и дополнительные аксиомы, соответственно, другого вида), придётся всё это добро вывести (только аксимы — правило выводится в §4.2).)

Как всё сложно. Правило обобщения мне из примеров вычленить не удалось — имеем нечто похожее (правила Бернайса) на то, что в вашей книге, по моей ссылке и в примерах исходных данных моего задания (хотя и есть некоторые сложности со странной заменой в одном из примеров (я это выделил в отдельное правило вывода в файле вычлененного), аксиомами формальной арифметики (кстати, почему о ней так сумбурно в английской Википедии?), замкнутостью условия (о ней выше), ограничивающими странностями в примерах (допустимое объявлено недопустимым (например, последние три строки файла «incorrect1.in», или файл «incorrect4.in» — но это уже далековато от темы)); ещё я не до конца уверен в правильности своей траковки требуемых условием «опциональных» сообщений об ошибках (есть в файле чуть выше)). Схемы аксиом одинаковы что в Википедии, что в вашей книге, что по моей ссылке выше, что в примерах исходных данных моего задания.

Вернёмся к первому абзацу. Я прочитал нужную часть вашей книги — там описывается как раз моя проблема (с. 142). Некоторые сложности вызывает то, что я слаб в намеченных там пропозициональных тавтологиях, но с другой стороны мне кажется, что я понимаю связанность переменных (а это важнее). Буду благодарен за помощь в выводе нужных тавтологий (одну из которых уже вроде вывел warlock66613).

(Оффтоп)

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

Kosat в сообщении #1009852

писал(а):
Ваш быстрый ум Kosat в сообщении #1009852

писал(а):
Уверен, это один из тех вопросов, которые легко решит человек, владеющий таинством логических формул. Да куда уж «владеющий таинством». Не переоценивайте людей, они от этого портятся. Я вам и помочь-то смог в прошлый раз по чистой случайности.

Есть мнение, что маслом кашу не испортишь. Но это лишь мнение.

[arseniiv]

Kosat в сообщении #1010530 писал(а):

$B$ может быть результатом применения одного из правил Бернайса. Это и есть моей проблемой.

Но не в случае 1 б), когда правила не к чему применять! Дальше — да.

Kosat в сообщении #1010530 писал(а):

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

Можно по правилу Gen их доводить до замкнутых — но тогда на это должны тратиться отдельные шаги вывода… Да и, ясно, сам вывод, из которой теоремой о дедукции строился другой, в том виде, в котором был, перестанет годиться. Странно предположить непоследовательность заданий, потому что они, наверно, всё-таки проверялись и не раз.

Kosat в сообщении #1010530 писал(а):

кстати, почему о ней так сумбурно в английской Википедии?

Не читал, а что конкретно не так?

Kosat в сообщении #1010530 писал(а):

странной заменой в одном из примеров (я это выделил в отдельное правило вывода в файле вычлененного
)

С какой? Там много, весь сканировать глазами…

Kosat в сообщении #1010530 писал(а):

допустимое объявлено недопустимым (например, последние три строки файла «incorrect1.in», или файл «incorrect4.in» — но это уже далековато от темы)

Тоже не нашёл в них ничего предосудительного.

Так, пропозициональные тавтологии. Требуется найти выводы $\chi\to(\psi\to\varphi)\vdash\chi\wedge\psi\to\varphi$, $\chi\wedge\psi\to\varphi\vdash\chi\to(\psi\to\varphi)$, $\chi\to(\varphi\to\psi)\vdash\varphi\to(\chi\to\psi)$. Последнюю действительно кто-то доказал, но, вроде, не warlock66613 (в этой теме как будто нет), хотя не важно. Я пытался доказать первые, но пытался плохо, потому что теоремы о дедукции не было. Теперь она есть, и всё просто ($\chi\to(\psi\to\varphi),\chi\wedge\psi\vdash\varphi$ в 8 шагов и $\chi\wedge\psi\to\varphi,\chi,\psi\vdash\varphi$ в 7 шагов, и дедукцией приводим к выводам того, что выше). Можно даже передоказать $\chi\to(\varphi\to\psi)\vdash\varphi\to(\chi\to\psi)$ через $\chi\to(\varphi\to\psi),\varphi,\chi\vdash\psi$ (5 шагов).

Может, не нужно показывать? (Или тогда выберите, какую из них; аксиомы нужны 3 в одном, 6 и 7 в другом и никаких в последнем.) Самое-то сложное в переписывании одного вывода в другой (в последних двух случаях аж по два применения теоремы). Если оно не автоматизировано.

-- Вс май 03, 2015 03:23:54 --

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

Требуется найти выводы

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

[Kosat]

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

Но что делать с примерами исходных данных моего задания с ошибками по замкнутости этих сущностей, все равно не понятно. Можно по правилу Gen их доводить до замкнутых — но тогда на это должны тратиться отдельные шаги вывода… Да и, ясно, сам вывод, из которой теоремой о дедукции строился другой, в том виде, в котором был, перестанет годиться.

Это да. В чём вообще разница между свободной переменной и переменной под квантором всеобщности? В человеческом смысле?

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

Странно предположить непоследовательность заданий, потому что они, наверно, всё-таки проверялись и не раз.

Так они формировались машинным образом, видимо (судя по чехарде со скобками в некоторых из них). Мелкие баги и фичи всегда присутствуют.

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

Kosat в сообщении #1010607 писал(а):

кстати, почему о ней так сумбурно в английской Википедии?

Не читал, а что конкретно не так?

https://en.wikipedia.org/wiki/Peano_axioms
https://ru.wikipedia.org/wiki/%D0%90%D0 ... 0%BD%D0%BE
В русской короче, но с математическими символами. Может я и не прав.

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

Kosat в сообщении #1010607 писал(а):

странной заменой в одном из примеров (я это выделил в отдельное правило вывода в файле вычлененного)

С какой? Там много, весь сканировать глазами…

$$FOL \ RR$$ $$@x((@yP(y))&Q(x)) \to (@yP(y))&Q(x)$$ $$@x((@xP(x))&Q(x)) \to (@xP(x))&Q(x)$$

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

Kosat в сообщении #1010607 писал(а):

допустимое объявлено недопустимым (например, последние три строки файла «incorrect1.in», или файл «incorrect4.in» — но это уже далековато от темы)

Тоже не нашёл в них ничего предосудительного.

Да, есть похожее в файлах «correct» - например:

$$@xP(x) \to P(x)$$ $$@xP(x) \to @xP(x)$$

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

Так, пропозициональные тавтологии. Требуется найти выводы $\chi\to(\psi\to\varphi)\vdash\chi\wedge\psi\to\varphi$, $\chi\wedge\psi\to\varphi\vdash\chi\to(\psi\to\varphi)$, $\chi\to(\varphi\to\psi)\vdash\varphi\to(\chi\to\psi)$. Последнюю действительно кто-то доказал, но, вроде, не warlock66613 (в этой теме как будто нет), хотя не важно.

Да, он лишь сказал, что «формулы $A \wedge B \to C$ и $A \to (B \to C)$ с обычной, неформальной, человеческой точки зрения - это одно и то же». Я ошибся.

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

Я пытался доказать первые, но пытался плохо, потому что теоремы о дедукции не было. Теперь она есть, и всё просто ($\chi\to(\psi\to\varphi),\chi\wedge\psi\vdash\varphi$ в 8 шагов и $\chi\wedge\psi\to\varphi,\chi,\psi\vdash\varphi$ в 7 шагов, и дедукцией приводим к выводам того, что выше). Можно даже передоказать $\chi\to(\varphi\to\psi)\vdash\varphi\to(\chi\to\psi)$ через $\chi\to(\varphi\to\psi),\varphi,\chi\vdash\psi$ (5 шагов).

Может, не нужно показывать? (Или тогда выберите, какую из них; аксиомы нужны 3 в одном, 6 и 7 в другом и никаких в последнем.) Самое-то сложное в переписывании одного вывода в другой (в последних двух случаях аж по два применения теоремы). Если оно не автоматизировано.

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

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

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

Непонятно.

[arseniiv]

Kosat в сообщении #1010727 писал(а):

В чём вообще разница между свободной переменной и переменной под квантором всеобщности? В человеческом смысле?

Значение формулы со свободными переменными зависит не только от интерпретации, но и от значений тех переменных. Если мы аналогично для таких «параметрических» интерпретаций определяем общезначимость и пр., тогда общезначимость формулы $\psi$ эквивалентна общезначимости формулы $\forall x.\,\psi$, где $x$ — любая переменная. Просто по определению значения формулы с квантором общезначимости. Потому даже иногда для краткости замкнутую формулу вида $\forall v_1.\forall v_2\ldots\forall v_n.\,\psi$, где в $\psi$ не содержит $\forall$, «сокращают» как $\psi$, подразумевая все опущеные кванторы.

Kosat в сообщении #1010727 писал(а):

https://en.wikipedia.org/wiki/Peano_axioms
https://ru.wikipedia.org/wiki/%D0%90%D0 ... 0%BD%D0%BE
В русской короче, но с математическими символами. Может я и не прав.

В английской в § First-order theory of arithmetic есть ну почти нормальная формулировка (зачем ограниченные кванторы в теории, где, во-первых, нет $\in$, а, во-вторых, и нужды в них; зачем так страшно формулировать схему индукции, когда есть простое обозначение замены в формуле). В русской тоже ничего лучше, и притом нет полезных объяснений для людей. Получается, русская всё-таки хуже.

Kosat в сообщении #1010727 писал(а):

FOL \ RR
@x((@yP(y))&Q(x)) \to (@yP(y))&Q(x)
@x((@xP(x))&Q(x)) \to (@xP(x))&Q(x)

А, ну это просто замена связанной переменной в кванторе. Она бывает нужна, чтобы мы могли совершить некорректную для предыдущей формулы подстановку. Есть все основания считать формулу, полученную такой заменой, эквивалентной предыдущей, хотя можно и оформить это дополнительным правилом вывода.

Kosat в сообщении #1010727 писал(а):

У меня же нет теоремы о дедукции.

«Пропозициональная»-то есть. Это для предикатов мы её ещё не получили. Вот, имея три нужных вывода, мы её получим, и вы сможете использовать её там где просят программой построить из $\Gamma,\varphi\vdash\psi$ вывод $\Gamma\vdash\varphi\to\psi$.

Kosat в сообщении #1010727 писал(а):

Непонятно.

Раз мы используем тавтологию $\alpha\to\beta$ лишь для того, чтобы вывести $\beta$ из $\alpha$, то нет смысла искать вывод $\vdash\alpha\to\beta$, т. к. к нему потом придётся добавлять ещё две строки — $\alpha$ и $\beta$ по MP из $\alpha\to\beta$ и $\alpha$. Если же мы нашли вывод $\alpha\vdash\beta$, нам не надо добавлять строки. В любом случае, это был просто комментарий к тому, что выше, если бы у вас были вопросы по тому, почему именно такие выводы нужны, а не другие.

[Kosat]

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

Значение формулы со свободными переменными зависит не только от интерпретации, но и от значений тех переменных. Если мы аналогично для таких «параметрических» интерпретаций определяем общезначимость и пр., тогда общезначимость формулы $\psi$ эквивалентна общезначимости формулы $\forall x.\,\psi$, где $x$ — любая переменная. Просто по определению значения формулы с квантором общезначимости. Потому даже иногда для краткости замкнутую формулу вида $\forall v_1.\forall v_2\ldots\forall v_n.\,\psi$, где в $\psi$ не содержит $\forall$, «сокращают» как $\psi$, подразумевая все опущеные кванторы.

Ответ непонятен, извините.

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

FOL \ RR
@x((@yP(y))&Q(x)) \to (@yP(y))&Q(x)
@x((@xP(x))&Q(x)) \to (@xP(x))&Q(x)
А, ну это просто замена связанной переменной в кванторе. Она бывает нужна, чтобы мы могли совершить некорректную для предыдущей формулы подстановку. Есть все основания считать формулу, полученную такой заменой, эквивалентной предыдущей, хотя можно и оформить это дополнительным правилом вывода.

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

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

У меня же нет теоремы о дедукции. «Пропозициональная»-то есть. Это для предикатов мы её ещё не получили. Вот, имея три нужных вывода, мы её получим, и вы сможете использовать её там где просят программой построить из $\Gamma,\varphi\vdash\psi$ вывод $\Gamma\vdash\varphi\to\psi$.

Доказательство пропозицинальной долго и конструктивно. Основывается на выводе исходного высказывания, которого (вывода) нет. Вот примеры исходных данных для всех заданий - там всё через схемы аксиом и правила вывода, а не через теоремы.

[arseniiv]

Kosat в сообщении #1011007 писал(а):

Ответ непонятен, извините.

Разумеется, извиняю. Только, если можете, скажите подробнее — может, непонятен не весь целиком, а какие-то части? Общезначимость формулы — известная вещь? Интерпретация [замкнутой] формулы?

Kosat в сообщении #1011007 писал(а):

Компьютер поймёт это только через правило вывода.

Угу, в вашей ситуации это действительно самый удобный способ — лишние сущности вводить не придётся. Жалко только, что это не описали в пояснении к заданию. Хотя, впрочем, уже и так непоняток достаточно — одной больше, одной меньше…

Kosat в сообщении #1011007 писал(а):

там всё через схемы аксиом и правила вывода, а не через теоремы

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

[Kosat]

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

Разумеется, извиняю. Только, если можете, скажите подробнее — может, непонятен не весь целиком, а какие-то части? Общезначимость формулы — известная вещь? Интерпретация [замкнутой] формулы?

Интерпретация [замкнутой] формулы. А ещё понятнее можно?

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

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

Вывести это нужно не через теоремы. Иначе тот же анализатор первого задания не поймёт.

[arseniiv]

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

Kosat в сообщении #1011234 писал(а):

А ещё понятнее можно?

Мне как-то неудобно отсылать к книге (уже знакомые Верещагин, Шень), но всё же почитайте там § 3.1—3.2, после чего любое количество вопросов задавайте — так будет немного проще, а то мне опять приходится угадывать, что неясно.

[Kosat]

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

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

Прочитал – хорошая книга. Понятная. Все равно не до самого конца ясно. В общем, из того, что я понял, «параметр» – это ещё один квантор всеобщности над уже существующими. Как бы операция наименьшего приоритета.

Но как соотносится прочитанное в книге с этим:

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

Если мы аналогично для таких «параметрических» интерпретаций определяем общезначимость и пр., тогда общезначимость формулы $\psi$ эквивалентна общезначимости формулы $\forall x.\,\psi$, где $x$ — любая переменная. Просто по определению значения формулы с квантором общезначимости. Потому даже иногда для краткости замкнутую формулу вида $\forall v_1.\forall v_2\ldots\forall v_n.\,\psi$, где в $\psi$ не содержит $\forall$, «сокращают» как $\psi$, подразумевая все опущеные кванторы.

?

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

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

Наша задача сейчас состоит в том, чтобы написать программу, проверяющую доказательство в формальной арифметике на корректность, а также преобразовывающую вывод $\Gamma, \alpha \vdash \beta$ в вывод $\Gamma \vdash \alpha \to \beta$.
Для последнего мы смотрим на доказательство теоремы о дедукции. Видим там как раз нужное преобразование выводов. Пытаемся его применить. То бишь для каждой строки $B_k$ получить строку $F_m \to B_k$. В случае с выводом строки $B_k$ с помощью одного из правил Бернайса нужно пройти несколько специфических пропозициональных преобразований. И тогда не то чтобы «теоремы о дедукции для исчисления предикатов (или для исчисления высказываний) тоже не будет», но наша задача по преобразованию вывода $\Gamma, \alpha \vdash \beta$ в вывод $\Gamma \vdash \alpha \to \beta$ будет решена.

[arseniiv]

Kosat в сообщении #1011574 писал(а):

В общем, из того, что я понял, «параметр» – это ещё один квантор всеобщности над уже существующими. Как бы операция наименьшего приоритета.

Не-не, параметрами там просто называются свободные переменные формулы — ведь её значение зависит от значений их и только их.

Kosat в сообщении #1011574 писал(а):

Но как соотносится прочитанное в книге с этим: <моя цитата>?

Там я просто употребил «параметрических» для понятности, потому и кавычки. Ведь такая интерпретация зависит ещё и от значений переменных. По счастью, входящих в параметры рассматриваемых формул.

Kosat в сообщении #1011574 писал(а):

Для последнего мы смотрим на доказательство теоремы о дедукции. Видим там как раз нужное преобразование выводов. Пытаемся его применить. То бишь для каждой строки $B_k$ получить строку $F_m \to B_k$. В случае с выводом строки $B_k$ с помощью одного из правил Бернайса нужно пройти несколько специфических пропозициональных преобразований.

Именно! А как мы эти пропозициональные преобразования можем выразить в выводе? Только выводом каких-то формул из других из имеющихся правил вывода. Вот я и предлагаю сделать такой вывод для формулы в общем случае — а потом мы будем его вставлять в выводы, которые программа должна построить, заменяя $\varphi,\chi,\psi$ на конкретные формулы. А чтобы получить такой «шаблон вывода», нам проще всего воспользоваться пропозициональной теоремой о дедукции.

(Я вот даже от нетерпения вчера даже применил один раз теорему о дедукции к своему выводу $\chi\to\varphi\to\psi,\varphi,\chi\vdash\psi$, получив вывод $\chi\to\varphi\to\psi,\varphi\vdash\chi\to\psi$ такого вида (выделены номера формул, полученных из формул оригинального вывода, так что можно отделить их от добавленного «клея»):

$$\begin{array}{lll} 1. & (\chi\to\chi\to\chi)\to(\chi\to(\chi\to\chi)\to\chi)\to(\chi\to\chi) & A_2 \\ 2. & \chi\to\chi\to\chi & A_1 \\ 3. & (\chi\to(\chi\to\chi)\to\chi)\to(\chi\to\chi) & \mathrm{MP}, 2, 1 \\ 4. & \chi\to(\chi\to\chi)\to\chi & A_1 \\ \mathbf5. & \chi\to\chi & \mathrm{MP}, 4, 3 \\ 6. & (\chi\to\varphi\to\psi)\to(\chi\to\chi\to\varphi\to\psi) & A_1 \\ 7. & \chi\to\varphi\to\psi & \mathrm{hyp.} \\ \mathbf8. & \chi\to\chi\to\varphi\to\psi & \mathrm{MP}, 7, 6 \\ 9. & (\chi\to\chi)\to(\chi\to\chi\to\varphi\to\psi)\to(\chi\to\varphi\to\psi) & A_2 \\ 10. & (\chi\to\chi\to\varphi\to\psi)\to(\chi\to\varphi\to\psi) & \mathrm{MP}, 5, 9 \\ \mathbf{11}. & \chi\to\varphi\to\psi & \mathrm{MP}, 8, 10 \\ 12. & \varphi\to\chi\to\varphi & A_1 \\ 13. & \varphi & \mathrm{hyp.} \\ \mathbf{14}. & \chi\to\varphi & \mathrm{MP}, 13, 12 \\ 15. & (\chi\to\varphi)\to(\chi\to\varphi\to\psi)\to(\chi\to\psi) & A_2 \\ 16. & (\chi\to\varphi\to\psi)\to(\chi\to\psi) & \mathrm{MP}, 14, 15 \\ \mathbf{17}. & \chi\to\psi & \mathrm{MP}, 11, 16 \\ \end{array}$$

И вам осталось всего 4 (ещё одно тут, одно там и два в третьем месте) из 5 применений теоремы.)

Если будет непонятно, как использовать одни выводы внутри другого, я с радостью поясню — но для этого нужны хоть какие-то готовые выводы из тех для примера. Впрочем, я могу состряпать пример использования вывода $\alpha,\beta\vdash\alpha\wedge\beta$ в, например, выводе $\alpha,\beta,\gamma\vdash(\alpha\wedge\beta)\wedge\gamma$, если захотите.

[Kosat]

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

Kosat в сообщении #1011574 писал(а):

В общем, из того, что я понял, «параметр» – это ещё один квантор всеобщности над уже существующими. Как бы операция наименьшего приоритета.

Не-не, параметрами там просто называются свободные переменные формулы — ведь её значение зависит от значений их и только их.

Ну да, я как раз и пытаюсь понять разницу между свободными переменными и переменными под квантором всеобщности. Так что фраза «параметрами там просто называются свободные переменные формулы» мало что объясняет в этом плане.

Kosat в сообщении #1011574 писал(а):

Но как соотносится прочитанное в книге с этим:

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

Если мы аналогично для таких «параметрических» интерпретаций определяем общезначимость и пр., тогда общезначимость формулы $\psi$ эквивалентна общезначимости формулы $\forall x.\,\psi$, где $x$ — любая переменная»?

Там я просто употребил «параметрических» для понятности, потому и кавычки. Ведь такая интерпретация зависит ещё и от значений переменных. По счастью, входящих в параметры рассматриваемых формул.

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

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

Kosat в сообщении #1011574 писал(а):

Для последнего мы смотрим на доказательство теоремы о дедукции. Видим там как раз нужное преобразование выводов. Пытаемся его применить. То бишь для каждой строки $B_k$ получить строку $F_m \to B_k$. В случае с выводом строки $B_k$ с помощью одного из правил Бернайса нужно пройти несколько специфических пропозициональных преобразований.

Именно! А как мы эти пропозициональные преобразования можем выразить в выводе? Только выводом каких-то формул из других из имеющихся правил вывода. Вот я и предлагаю сделать такой вывод для формулы в общем случае — а потом мы будем его вставлять в выводы, которые программа должна построить, заменяя $\varphi,\chi,\psi$ на конкретные формулы. А чтобы получить такой «шаблон вывода», нам проще всего воспользоваться пропозициональной теоремой о дедукции.

(Я вот даже от нетерпения вчера даже применил один раз теорему о дедукции к своему выводу $\chi\to\varphi\to\psi,\varphi,\chi\vdash\psi$, получив вывод $\chi\to\varphi\to\psi,\varphi\vdash\chi\to\psi$ такого вида (выделены номера формул, полученных из формул оригинального вывода, так что можно отделить их от добавленного «клея»):

$$\begin{array}{lll} 1. & (\chi\to\chi\to\chi)\to(\chi\to(\chi\to\chi)\to\chi)\to(\chi\to\chi) & A_2 \\ 2. & \chi\to\chi\to\chi & A_1 \\ 3. & (\chi\to(\chi\to\chi)\to\chi)\to(\chi\to\chi) & \mathrm{MP}, 2, 1 \\ 4. & \chi\to(\chi\to\chi)\to\chi & A_1 \\ \mathbf5. & \chi\to\chi & \mathrm{MP}, 4, 3 \\ 6. & (\chi\to\varphi\to\psi)\to(\chi\to\chi\to\varphi\to\psi) & A_1 \\ 7. & \chi\to\varphi\to\psi & \mathrm{hyp.} \\ \mathbf8. & \chi\to\chi\to\varphi\to\psi & \mathrm{MP}, 7, 6 \\ 9. & (\chi\to\chi)\to(\chi\to\chi\to\varphi\to\psi)\to(\chi\to\varphi\to\psi) & A_2 \\ 10. & (\chi\to\chi\to\varphi\to\psi)\to(\chi\to\varphi\to\psi) & \mathrm{MP}, 5, 9 \\ \mathbf{11}. & \chi\to\varphi\to\psi & \mathrm{MP}, 8, 10 \\ 12. & \varphi\to\chi\to\varphi & A_1 \\ 13. & \varphi & \mathrm{hyp.} \\ \mathbf{14}. & \chi\to\varphi & \mathrm{MP}, 13, 12 \\ 15. & (\chi\to\varphi)\to(\chi\to\varphi\to\psi)\to(\chi\to\psi) & A_2 \\ 16. & (\chi\to\varphi\to\psi)\to(\chi\to\psi) & \mathrm{MP}, 14, 15 \\ \mathbf{17}. & \chi\to\psi & \mathrm{MP}, 11, 16 \\ \end{array}$$

И вам осталось всего 4 (ещё одно тут, одно там и два в третьем месте) из 5 применений теоремы.)

Если будет непонятно, как использовать одни выводы внутри другого, я с радостью поясню — но для этого нужны хоть какие-то готовые выводы из тех для примера. Впрочем, я могу состряпать пример использования вывода $\alpha,\beta\vdash\alpha\wedge\beta$ в, например, выводе $\alpha,\beta,\gamma\vdash(\alpha\wedge\beta)\wedge\gamma$, если захотите.

Может я действительно чего-то не понимаю. Преобразуйте вывод $\Gamma, \alpha \vdash \beta$ в вывод $\Gamma \vdash \alpha \to \beta$ на примере этого вывода:

$$A \rightarrow B \vdash A \rightarrow \forall x B $$ $$\begin{array}{lll} 1. & A \rightarrow B & Hyp. \ 1\\ 2. & A \rightarrow \forall x B & BR \ 1, \ 1\\ \end{array}$$

[Kosat]

Интересно сказано также на странице 157:
"С этим связан и другой выбор: как определять истинность формул. Тут есть две возможности: можно определять истинность формулы на оценке (при данных значениях параметров), а можно говорить только о замкнутых формулах, вводя константы для всех элементов интерпретации. И тот, и другой способы имеют недостатки, а выбор нами первого подхода — результат не единодушия авторов, а волевого решения."

[arseniiv]

Kosat в сообщении #1011628 писал(а):

Ну да, я как раз и пытаюсь понять разницу между свободными переменными и переменными под квантором всеобщности. Так что фраза «параметрами там просто называются свободные переменные формулы» мало что объясняет в этом плане.

А, это. Раз значение формулы не зависит от значений переменных, которые в ней связаны, то можно считать, что их в ней вообще нет: вы уже видели эквивалентность формул $\mathsf Qx.\,\varphi$ и $\mathsf Qy.\,\varphi[y/x]$. Использование кванторов с переменными — это просто более частое из двух соглашений, оба из которых ведут к своим неудобствам при описании (это — к недопустимым заменам); другое соглашение — это индексы де Брёйна (de Bruijn) [не смотрите на λ-исчисление, они применимы и здесь], и дня него, в свою очередь, при подстановке надо сделать кое-какие действия с индексами и вообще иметь расширенный для этого синтаксис формул. Зато нет необходимости в переименовании связанных переменных, и две эквивалентные по такому преобразованию формулы в таком случае переводятся в одну и ту же.

Kosat в сообщении #1011628 писал(а):

Может я действительно чего-то не понимаю. Преобразуйте вывод $\Gamma, \alpha \vdash \beta$ в вывод $\Gamma \vdash \alpha \to \beta$ на примере этого вывода:

$$ A \rightarrow B \vdash A \rightarrow \forall x B $$ $$ A \rightarrow B $$ $$ A \rightarrow \forall x B $$

Этого я как раз сделать сейчас не могу, потому что у меня нет выводов $\chi\to\psi\to\varphi\vdash\chi\wedge\psi\to\varphi$, $\chi\wedge\psi\to\varphi\vdash\chi\to\psi\to\varphi$. Могу только показать «шаблон» вывода:

$$\begin{array}{lll} \boldsymbol i_{\mathbf1}. & (A\to B)\to A\to B & \mathrm{inc.}~{}\vdash\varphi\to\varphi \\ i_2. & (A\to B)\wedge A\to B & \mathrm{inc.}~\chi\to\psi\to\varphi\vdash\chi\wedge\psi\to\varphi,\; i_1 \\ i_3. & (A\to B)\wedge A\to\forall x.\,B & \mathrm B_\forall,\; i_2 \\ \boldsymbol i_{\mathbf4}. & (A\to B)\to A\to\forall x.\,B & \mathrm{inc.}~\chi\wedge\psi\to\varphi\vdash\chi\to\psi\to\varphi,\; i_3 \\ \end{array}$$

(Но в книге вы нечто подобное и так видели, так что вряд ли это ново.) Пометка «inc[lude]. $\Gamma\vdash\varphi$, номера» тут означает, что мы выше помеченной формулы включили (но не показали здесь — оттого индексы у меня не конкретные числа) вывод, которым было доказано $\Gamma\vdash\varphi$, во всех его формулах сделав одинаковые замены так, чтобы гипотезы превратились в формулы нашего вывода по указанным номерам,* а $\varphi$ превратилась в формулу, которая помечена этим самым inc.. Это не более чем сокращённая запись, если использованные выводимости у нас до этого уже были показаны. Как раз-таки две последние пока здесь и не показаны!

* Если гипотезы в inc-выводе стоят не в том же порядке, что формулы у нас в шаблоне, мы переставляем куски одного из выводов соответствующим образом; такое действие не влияет на корректность вывода, т. к., по сути, это укладка специального вида орграфа в «массив» (наверно, вы видели, как бинарные деревья иногда представляют массивом, а не динамической структурой с блоками где попало в виртуальной памяти), и частичный порядок, задаваемый этим графом, можно дополнить до линейного порой не единственным способом. В принципе, если все выводы строить специальным образом, то переставление кусков, вроде, не понадобится. (Если это заинтересовало, но не понятно, обсудим ниже этого поста. Вам такая процедура не понадобится, потому что наши пропозициональные штучки имеют по одной гипотезе, и их выводы мы сразу сделаем так, чтобы эта гипотеза была самой первой. В таком случае никаких смещений не нужно.)

Как $\mathrm B_\forall$ я обозначил первое правило Бернайса.

И вот чтобы понять, как по такому шаблону получить вывод, я и предлагал те штучки с конъюнкциями в предыдущем посте. Вот как это сработает с ними.

Вывод $\alpha,\beta\vdash\alpha\wedge\beta$ простой:

$$\begin{array}{lll} a. & \alpha & \mathrm{hyp.} \\ b. & \alpha\to\beta\to\alpha\wedge\beta & A_3 \\ c. & \beta\to\alpha\wedge\beta & \mathrm{MP}, a, b \\ d. & \beta & \mathrm{hyp.} \\ e. & \alpha\wedge\beta & \mathrm{MP}, d, c \\ \end{array}$$

(Формулы я пронумеровал буквами для будущего удобства.)

Вывод $\alpha,\beta,\gamma\vdash(\alpha\wedge\beta)\wedge\gamma$ можно составить теперь такой:

$$\begin{array}{lll} i_1. & \alpha & \mathrm{hyp.} \\ i_2. & \beta & \mathrm{hyp.} \\ i_3. & \alpha\wedge\beta & \mathrm{inc.}~\alpha,\beta\vdash\alpha\wedge\beta,\; i_1, i_2 \\ i_4 & \gamma & \mathrm{hyp.} \\ i_5. & (\alpha\wedge\beta)\wedge\gamma & \mathrm{inc.}~\alpha,\beta\vdash\alpha\wedge\beta,\; i_3, i_4\quad\text{(подстановка }\alpha\wedge\beta/\alpha, \gamma/\beta\text{)} \\ \end{array}$$

Зная вывод $\alpha,\beta\vdash\alpha\wedge\beta$, мы теперь можем его корректно вставить. Я сделаю два столбца индексов, дополнительно показывая индексы формул из этого вывода, заменой которых получились конечные.

$$\begin{array}{llll} 1 = i_1. & a & \alpha & \mathrm{hyp.} \\ 2. & b & \alpha\to\beta\to\alpha\wedge\beta & A_3 \\ 3. & c & \beta\to\alpha\wedge\beta & \mathrm{MP}, 1/a, 2/b \\ 4 = i_2. & d & \beta & \mathrm{hyp.} \\ 5 = i_3. & e, a' & \alpha\wedge\beta & \mathrm{MP}, 4/d, 3/c \\ 6. & b' & \alpha\wedge\beta\to\gamma\to(\alpha\wedge\beta)\wedge\gamma & A_3 \\ 7. & c' & \gamma\to(\alpha\wedge\beta)\wedge\gamma & \mathrm{MP}, 5/a', 6/b' \\ 8 = i_4. & d' & \gamma & \mathrm{hyp.} \\ 9 = i_5. & e' & (\alpha\wedge\beta)\wedge\gamma & \mathrm{MP}, 8/d', 7/c' \\ \end{array}$$

Всё! Получен корректный вывод $\alpha,\beta,\gamma\vdash(\alpha\wedge\beta)\wedge\gamma$.

Как здесь видно, «inc-сокращения» в использовании неотличимы от правил вывода. Мы можем предположить, что такие правила (производные правила вывода) у нас действительно есть наряду с MP и правилами Бернайса, и выводить с помощью них что-нибудь — а потом мы просто воспринимаем полученный вывод как сокращение, а вместо применений производных правил вставлять соответствующие выводы как это делалось выше. Надеюсь, вы о производных правилах вывода уже где-нибудь читали, но просто не успели составить картину.

Если применения правил вывода сравнить с вызовами функций (а аксиомы — константы), то разворачивание производных правил вывода аналогично компиляции inline-функций, код которых с соответствующими изменениями засовывается прямо в вызывающий код. Кстати, в подобной аналогии можно последнюю формулу вывода обозвать результатом, а гипотезы — аргументами какой-то функции. (В результате мы получили кривенькую аналогию изоморфизма Карри—Говарда, но про него уже другая история. )

-- Ср май 06, 2015 03:23:54 --

(Оффтоп)

Оказалось, я скопировал недоредактированный вывод из вашего сообщения. Надеюсь, вы не против, если я его не буду менять у себя (и так сто лет писал ).

-- Ср май 06, 2015 03:39:45 --

Ах да, чтобы не отрываться от смысла: когда математик говорит: «то-то и то-то по теореме такой-то» — он как раз использует производное правило вывода, подразумевая, что тот результат, где это всё он упомянул, можно переписать так, чтобы получился обычный вывод из одних только аксиом и гипотез теории. Корректность такого вывода притом зависит только от корректности вывода с производными правилами и корректности выводов, соответствующих самим этим правилам, и потому мы даже не пытаемся всё развернуть (и, наоборот, пытаемся отрефакторить всё так, чтобы выводы были поминиатюрнее, потому что в человеческую голову сразу много не влезает). Обычный математический текст можно понимать как много-много сокращений сначала введением производных правил в формальный вывод, а потом ещё приведением полученного вывода в читаемую форму с использованием остальной информации из контекста (и влияя на него тоже).

UPD: Исправил оригинальное написание де Брёйна.

[Kosat]

Я долго редактирую, такой недостаток (зато здесь быстро прекращают давать это делать). Спасибо за много полезной информации, различные выводы. Нечто похожее на "производные правила вывода" были у меня и во втором задании - суть всё та же, разворачивание строк до применения теоремы о дедукции в строки после её применения (там они были не особо длинные - минимум одна-в-три). Программировать это сложно, но можно. Мне по-прежнему нужны те несколько пропозициональных выводов, которые помогут обработать правила Бернайса в теореме о дедукции исчисления высказываний...