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

[arseniiv]

Так, стоп, у вас уже есть программа, генерирующая вывод в соответствии с пропозициональной теоремой о дедукции? Если есть, так и загоните в неё

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

$$\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}$$

чтобы избавила от гипотезы $\varphi$. Получится код, который надо будет вписывать при переделке второго правила Бернайса два раза. Для первого правила сначала вручную напишите выводы для

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

$\chi\to(\psi\to\varphi),\chi\wedge\psi\vdash\varphi$ в 8 шагов и $\chi\wedge\psi\to\varphi,\chi,\psi\vdash\varphi$ в 7 шагов

и избавьтесь программой от гипотез $\chi\wedge\psi,\chi,\psi$. Получатся два вывода, вставляемые как раз в проиллюстрированном переписывании первого правила Бернайса.

-- Ср май 06, 2015 04:28:51 --

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

напишите выводы

Если забыл сказать, они пишутся почти что сами собой.

[Kosat]

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

Последний раз редактировалось arseniiv
06.05.2015, 02:36, всего редактировалось 3 раз(а).
Так, стоп, у вас уже есть программа, генерирующая вывод в соответствии с пропозициональной теоремой о дедукции? Если есть, так и загоните в неё

Эта программа не генерирует вывод с нуля, а преобразовывает вывод $\Gamma, \alpha \vdash \beta$ в вывод $\Gamma \vdash \alpha \to \beta$ . У нас нет "выводов с нуля" ни левой, ни правой части требуемых пропозициональных тождеств. Ваш длинный вывод вообще непонятно каким здесь боком.

[arseniiv]

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

Эта программа не генерирует вывод с нуля, а преобразовывает вывод $\Gamma, \alpha \vdash \beta$ в вывод $\Gamma \vdash \alpha \to \beta$ .

Да, с нуля получить вывод в нашем случае уже нельзя для всякой формулы — для каких-то любой алгоритм не завершится. Вот если убрать все не нульместные предикатные и вообще все функциональные символы… (и ещё есть много частных случаев). Так что этого я и не прошу, а только предлагаю преобразовать именно так — вывод $\chi\to\psi\to\varphi,\chi\wedge\psi\vdash\varphi$ в вывод $\chi\to\psi\to\varphi\vdash\chi\wedge\psi\to\varphi$ (и те два ещё), который потом надо записать в какой-то файл (ну или прямо в коде в какую-то переменную) и вставлять в генерируемые теоремой о дедукции первого порядка выводы (с заменами, конечно). И в последний раз, мне показалось, я уже выразил это ясно.

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

Ваш длинный вывод вообще непонятно каким здесь боком.

Ну как же непонятно каким, когда самым прямым (см. выше)!

Завтра ещё напишу, а сейчас пока не могу.

[Kosat]

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

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

Заставим. Надо только те пропозициональные тождества вывести.

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

Ну как же непонятно каким, когда самым прямым (см. выше)!
Завтра ещё напишу, а сейчас пока не могу.

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

[arseniiv]

(Оффтоп)

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

Заставим. Надо только те пропозициональные тождества вывести.

Среди заданий вроде не было вывода произвольной формулы с нуля, вы ж и сами говорили.

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

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

Вот те пропущеные действия и есть шаги вставляемого-с-подстановкой вывода, в том-то и дело! Чем они ещё могут быть? Применением какого-то одного неизвестного правила вывода — нам это не позволено.

-- Чт май 07, 2015 10:17:10 --

В общем, если появятся какие-то новые вопросы — поглядим, а так больше не могу сказать ничего нового. Может, кто-то скажет другими словами более понятно, но я уже всё перепробовал.

[Kosat]

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

Вот те пропущеные действия и есть шаги вставляемого-с-подстановкой вывода, в том-то и дело! Чем они ещё могут быть? Применением какого-то одного неизвестного правила вывода — нам это не позволено.

-- Чт май 07, 2015 10:17:10 --

В общем, если появятся какие-то новые вопросы — поглядим, а так больше не могу сказать ничего нового. Может, кто-то скажет другими словами более понятно, но я уже всё перепробовал.

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

P.S. Я догадываюсь, что вы изобрели какой-то "универсальный метод" и тщетно пытаетесь мне растолковать его применение для первого правила Бернайса. Но это снова наталкивается на необходимость выводов, которые ничуть не проще, и даже может быть сложнее тех, которые в книге:

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

Так, стоп, у вас уже есть программа, генерирующая вывод в соответствии с пропозициональной теоремой о дедукции? Если есть, так и загоните в неё

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

$$\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}$$

чтобы избавила от гипотезы $\varphi$. Получится код, который надо будет вписывать при переделке второго правила Бернайса два раза. Для первого правила сначала вручную напишите выводы для

$\chi\to(\psi\to\varphi),\chi\wedge\psi\vdash\varphi$ в 8 шагов и $\chi\wedge\psi\to\varphi,\chi,\psi\vdash\varphi$ в 7 шагов и избавьтесь программой от гипотез $\chi\wedge\psi,\chi,\psi$. Получатся два вывода, вставляемые как раз в проиллюстрированном переписывании первого правила Бернайса.

[arseniiv]

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

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

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

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

P.S. Я догадываюсь, что вы изобрели какой-то "универсальный метод" и тщетно пытаетесь мне растолковать его применение для первого правила Бернайса.

Вряд ли даже переизобрёл — просто сложил два и два. Уверен, через какое-то время и вам это станет более-менее очевидно.

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

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

В общем случае нет. В книге кусок вывода, соответствующий применению эквивалентности пропозициональных формул, опущен только из-за доказанной раньше теоремы о $\Gamma\vdash\varphi\Leftrightarrow\Gamma\vDash\varphi$ для исчисления высказываний, и конструирование вывода возложено на неё (и с ним справится в данном случае программа при любом корректном входе).

[Kosat]

Все равно, честно, не вижу связи между всеми вашими выводами и требуемыми. Но я сделал всё, о чём вы говорили.

Нумерованный первоначальный первый:

$$X \to Y \to Z,Y|-X \to Z $$ $$\begin{array}{lll} (1) & (X \to X \to X) \to (X \to (X \to X) \to X) \to (X \to X) & (SoA \ 2) \\ (2) & X \to X \to X & (SoA \ 1) \\ (3) & (X \to (X \to X) \to X) \to (X \to X) & (M.P. \ 2, 1) \\ (4) & X \to (X \to X) \to X & (SoA \ 1) \\ (5) & X \to X & (M.P. \ 4, 3) \\ (6) & (X \to Y \to Z) \to (X \to X \to Y \to Z) & (SoA \ 1) \\ (7) & X \to Y \to Z & (Hyp. \ 1) \\ (8) & X \to X \to Y \to Z & (M.P. \ 7, 6) \\ (9) & (X \to X) \to (X \to X \to Y \to Z) \to (X \to Y \to Z) & (SoA \ 2) \\ (10) & (X \to X \to Y \to Z) \to (X \to Y \to Z) & (M.P. \ 5, 9) \\ (11) & X \to Y \to Z & (Hyp. \ 1) \\ (12) & Y \to X \to Y & (SoA \ 1) \\ (13) & Y & (Hyp. \ 2) \\ (14) & X \to Y & (M.P. \ 13, 12) \\ (15) & (X \to Y) \to (X \to Y \to Z) \to (X \to Z) & (SoA \ 2) \\ (16) & (X \to Y \to Z) \to (X \to Z) & (M.P. \ 14, 15) \\ (17) &X \to Z & (M.P. \ 7, 16) \\ \end{array}$$

 

Нумерованный модифицированный первый:

$$X \to Y \to Z|-(Y) \to X \to Z $$ $$\begin{array}{lll} (1) & (X \to X \to X) \to (X \to (X \to X) \to X) \to (X \to X) & (SoA \ 2) \\ (2) & ((X \to X \to X) \to (X \to (X \to X) \to X) \to & (SoA \ 1) \\ & (X \to X)) \to ((Y) \to (X \to X \to X) \to & \\ & (X \to (X \to X) \to X) \to (X \to X)) & \\ (3) & (Y) \to (X \to X \to X) \to (X \to (X \to X) \to X) \to (X \to X) & (M.P. \ 1, 2) \\ (4) & X \to X \to X & (SoA \ 1) \\ (5) & (X \to X \to X) \to ((Y) \to X \to X \to X) & (SoA \ 1) \\ (6) & (Y) \to X \to X \to X & (M.P. \ 4, 5) \\ (7) & ((Y) \to X \to X \to X) \to ((Y) \to (X \to X \to X) & (SoA \ 2) \\ & \to (X \to (X \to X) \to X) \to (X \to X)) \to ((Y) & \\ & \to (X \to (X \to X) \to X) \to (X \to X)) & \\ (8) & ((Y) \to ((X \to X \to X) \to (X \to (X \to X) \to X) \to (X \to X))) \to ((Y) \to & (M.P. \ 6, 7) \\ & (X \to (X \to X) \to X) \to (X \to X)) & \\ (9) & (Y) \to (X \to (X \to X) \to X) \to (X \to X) & (M.P. \ 3, 8) \\ (10) & X \to (X \to X) \to X & (SoA \ 1) \\ (11) & (X \to (X \to X) \to X) \to ((Y) \to X \to (X \to X) \to X) & (SoA \ 1) \\ (12) & (Y) \to X \to (X \to X) \to X & (M.P. \ 10, 11) \\ (13) & ((Y) \to X \to (X \to X) \to X) \to ((Y) \to (X \to (X \to X) \to X) & (SoA \ 2) \\ & \to (X \to X)) \to ((Y) \to X \to X) & \\ (14) & ((Y) \to ((X \to (X \to X) \to X) \to X \to X)) \to ((Y) \to X \to X) & (M.P. \ 12, 13) \\ (15) & (Y) \to X \to X & (M.P. \ 9, 14) \\ (16) & (X \to Y \to Z) \to (X \to X \to Y \to Z) & (SoA \ 1) \\ (17) & ((X \to Y \to Z) \to (X \to X \to Y \to Z)) \to ((Y) & (SoA \ 1) \\ & \to (X \to Y \to Z) \to (X \to X \to Y \to Z)) & \\ (18) & (Y) \to (X \to Y \to Z) \to (X \to X \to Y \to Z) & (M.P. \ 16, 17) \\ (19) & X \to Y \to Z & (Hyp. \ 1) \\ (20) & (X \to Y \to Z) \to ((Y) \to X \to Y \to Z) & (SoA \ 1) \\ (21) & (Y) \to X \to Y \to Z & (M.P. \ 19, 20) \\ (22) & ((Y) \to X \to Y \to Z) \to ((Y) \to (X \to Y \to Z) \to & (SoA \ 2) \\ & (X \to X \to Y \to Z)) \to ((Y) \to X \to X \to Y \to Z) & \\ (23) & ((Y) \to ((X \to Y \to Z) \to X \to X \to Y \to Z)) \to ((Y) \to X \to X \to Y \to Z) & (M.P. \ 21, 22) \\ (24) & (Y) \to X \to X \to Y \to Z & (M.P. \ 18, 23) \\ (25) & (X \to X) \to (X \to X \to Y \to Z) \to (X \to Y \to Z) & (SoA \ 2) \\ (26) & ((X \to X) \to (X \to X \to Y \to Z) \to (X \to Y \to Z)) & (SoA \ 1) \\ & \to ((Y) \to (X \to X) \to (X \to X \to Y \to Z) \to (X \to Y \to Z)) & \\ (27) & (Y) \to (X \to X) \to (X \to X \to Y \to Z) \to (X \to Y \to Z) & (M.P. \ 25, 26) \\ (28) & ((Y) \to X \to X) \to ((Y) \to (X \to X) \to (X \to X \to Y \to Z) & (SoA \ 2) \\ & \to (X \to Y \to Z)) \to ((Y) \to (X \to X \to Y \to Z) \to (X \to Y \to Z)) & \\ (29) & ((Y) \to ((X \to X) \to (X \to X \to Y \to Z) \to (X \to Y \to Z))) & (M.P. \ 15, 28) \\ & \to ((Y) \to (X \to X \to Y \to Z) \to (X \to Y \to Z)) & \\ \end{array}$$

 

$$\begin{array}{lll} (30) & (Y) \to (X \to X \to Y \to Z) \to (X \to Y \to Z) & (M.P. \ 27, 29) \\ (31) & X \to Y \to Z & (Hyp. \ 1) \\ (32) & (X \to Y \to Z) \to ((Y) \to X \to Y \to Z) & (SoA \ 1) \\ (33) & (Y) \to X \to Y \to Z & (M.P. \ 19, 20) \\ (34) & Y \to X \to Y & (SoA \ 1) \\ (35) & (Y \to X \to Y) \to ((Y) \to Y \to X \to Y) & (SoA \ 1) \\ (36) & (Y) \to Y \to X \to Y & (M.P. \ 34, 35) \\ (37) & ((Y) \to ((Y) \to Y)) \to ((Y) \to (((Y) \to Y) \to Y)) \to ((Y) \to Y) & (SoA \ 2) \\ (38) & (Y) \to ((Y) \to Y) & (SoA \ 1) \\ (39) & ((Y) \to (((Y) \to Y) \to Y)) \to ((Y) \to Y) & (M.P. \ 38, 37) \\ (40) & (Y) \to (((Y) \to Y) \to Y) & (SoA \ 1) \\ (41) & (Y) \to Y & (M.P. \ 40, 39) \\ (42) & ((Y) \to Y) \to ((Y) \to Y \to X \to Y) \to ((Y) \to X \to Y) & (SoA \ 2) \\ (43) & ((Y) \to ((Y) \to X \to Y)) \to ((Y) \to X \to Y) & (M.P. \ 41, 42) \\ (44) & (Y) \to X \to Y & (SoA \ 1) \\ (45) & (X \to Y) \to (X \to Y \to Z) \to (X \to Z) & (SoA \ 2) \\ (46) & ((X \to Y) \to (X \to Y \to Z) \to (X \to Z)) & (SoA \ 1) \\ & \to ((Y) \to (X \to Y) \to (X \to Y \to Z) \to (X \to Z)) & \\ (47) & (Y) \to (X \to Y) \to (X \to Y \to Z) \to (X \to Z) & (M.P. \ 45, 46) \\ (48) & ((Y) \to X \to Y) \to ((Y) \to (X \to Y) \to (X \to Y \to Z) \to & (SoA \ 2) \\ & (X \to Z)) \to ((Y) \to (X \to Y \to Z) \to (X \to Z)) & \\ (49) & ((Y) \to ((X \to Y) \to (X \to Y \to Z) \to (X \to Z))) & (M.P. \ 34, 48) \\ & \to ((Y) \to (X \to Y \to Z) \to (X \to Z)) & \\ (50) & (Y) \to (X \to Y \to Z) \to (X \to Z) & (M.P. \ 47, 49) \\ (51) & ((Y) \to X \to Y \to Z) \to ((Y) \to (X \to Y \to Z) \to (X \to Z)) \to ((Y) \to X \to Z) & (SoA \ 2) \\ (52) & ((Y) \to ((X \to Y \to Z) \to X \to Z)) \to ((Y) \to X \to Z) & (M.P. \ 21, 51) \\ (53) & (Y) \to X \to Z & (M.P. \ 50, 52) \\ \end{array}$$

 
 
Нумерованный первоначальный второй:

$$X \to Y \to Z,X \wedge Y|-Z $$ $$\begin{array}{lll} (1) & X \wedge Y & (Hyp. \ 2) \\ (2) & X \wedge Y \to X & (SoA \ 3) \\ (3) & X & (M.P. \ 1, 2) \\ (4) & X \to Y \to Z & (Hyp. \ 1) \\ (5) & Y \to Z & (M.P. \ 3, 4) \\ (6) & X \wedge Y \to Y & (SoA \ 4) \\ (7) & Y & (M.P. \ 1, 6) \\ (8) & Z & (M.P. \ 7, 5) \\ \end{array}$$

Нумерованный модифицированный второй:

$$X \to Y \to Z|-(X \wedge Y) \to Z $$ $$\begin{array}{lll} (1) & ((X \wedge Y) \to ((X \wedge Y) \to X \wedge Y)) \to ((X \wedge Y) \to & (SoA \ 2) \\ & (((X \wedge Y) \to X \wedge Y) \to X \wedge Y)) \to ((X \wedge Y) \to X \wedge Y) & \\ (2) & (X \wedge Y) \to ((X \wedge Y) \to X \wedge Y) & (SoA \ 1) \\ (3) & ((X \wedge Y) \to (((X \wedge Y) \to X \wedge Y) \to X \wedge Y)) \to ((X \wedge Y) \to X \wedge Y) & (M.P. \ 2, 1) \\ (4) & (X \wedge Y) \to (((X \wedge Y) \to X \wedge Y) \to X \wedge Y) & (SoA \ 1) \\ (5) & (X \wedge Y) \to X \wedge Y & (M.P. \ 4, 3) \\ (6) & X \wedge Y \to X & (SoA \ 3) \\ (7) & (X \wedge Y \to X) \to ((X \wedge Y) \to X \wedge Y \to X) & (SoA \ 1) \\ (8) & (X \wedge Y) \to X \wedge Y \to X & (M.P. \ 6, 7) \\ (9) & ((X \wedge Y) \to X \wedge Y) \to ((X \wedge Y) \to X \wedge Y \to X) \to ((X \wedge Y) \to X) & (SoA \ 2) \\ (10) & ((X \wedge Y) \to ((X \wedge Y) \to X)) \to ((X \wedge Y) \to X) & (M.P. \ 5, 9) \\ (11) & (X \wedge Y) \to X & (SoA \ 3) \\ (12) & X \to Y \to Z & (Hyp. \ 1) \\ (13) & (X \to Y \to Z) \to ((X \wedge Y) \to X \to Y \to Z) & (SoA \ 1) \\ (14) & (X \wedge Y) \to X \to Y \to Z & (M.P. \ 12, 13) \\ (15) & ((X \wedge Y) \to X) \to ((X \wedge Y) \to X \to Y \to Z) \to ((X \wedge Y) \to Y \to Z) & (SoA \ 2) \\ (16) & ((X \wedge Y) \to ((X) \to Y \to Z)) \to ((X \wedge Y) \to Y \to Z) & (M.P. \ 6, 15) \\ (17) & (X \wedge Y) \to Y \to Z & (M.P. \ 14, 16) \\ (18) & X \wedge Y \to Y & (SoA \ 4) \\ (19) & (X \wedge Y \to Y) \to ((X \wedge Y) \to X \wedge Y \to Y) & (SoA \ 1) \\ (20) & (X \wedge Y) \to X \wedge Y \to Y & (M.P. \ 18, 19) \\ (21) & ((X \wedge Y) \to X \wedge Y) \to ((X \wedge Y) \to X \wedge Y \to Y) \to ((X \wedge Y) \to Y) & (SoA \ 2) \\ (22) & ((X \wedge Y) \to ((X \wedge Y) \to Y)) \to ((X \wedge Y) \to Y) & (M.P. \ 5, 21) \\ (23) & (X \wedge Y) \to Y & (SoA \ 4) \\ (24) & ((X \wedge Y) \to Y) \to ((X \wedge Y) \to Y \to Z) \to ((X \wedge Y) \to Z) & (SoA \ 2) \\ (25) & ((X \wedge Y) \to ((Y) \to Z)) \to ((X \wedge Y) \to Z) & (M.P. \ 18, 24) \\ (26) & (X \wedge Y) \to Z & (M.P. \ 17, 25) \\ \end{array}$$

Нумерованный первоначальный третий:

$$X \wedge Y \to Z,X,Y|-Z $$ $$\begin{array}{lll} (1) & X \to Y \to X \wedge Y & (SoA \ 5) \\ (2) & X & (Hyp. \ 2) \\ (3) & Y \to X \wedge Y & (M.P. \ 2, 1) \\ (4) & Y & (Hyp. \ 3) \\ (5) & X \wedge Y & (M.P. \ 4, 3) \\ (6) & X \wedge Y \to Z & (Hyp. \ 1) \\ (7) & Z & (M.P. \ 5, 6) \\ \end{array}$$

Нумерованный модифицированный третий:

$$X \wedge Y \to Z,X|-(Y) \to Z $ $$\begin{array}{lll} (1) & X \to Y \to X \wedge Y & (SoA \ 5) \\ (2) & (X \to Y \to X \wedge Y) \to ((Y) \to X \to Y \to X \wedge Y) & (SoA \ 1) \\ (3) & (Y) \to X \to Y \to X \wedge Y & (M.P. \ 1, 2) \\ (4) & X & (Hyp. \ 2) \\ (5) & (X) \to ((Y) \to X) & (SoA \ 1) \\ (6) & (Y) \to X & (M.P. \ 4, 5) \\ (7) & ((Y) \to X) \to ((Y) \to X \to Y \to X \wedge Y) \to ((Y) \to Y \to X \wedge Y) & (SoA \ 2) \\ (8) & ((Y) \to ((X) \to Y \to X \wedge Y)) \to ((Y) \to Y \to X \wedge Y) & (M.P. \ 6, 7) \\ (9) & (Y) \to Y \to X \wedge Y & (M.P. \ 3, 8) \\ (10) & ((Y) \to ((Y) \to Y)) \to ((Y) \to (((Y) \to Y) \to Y)) \to ((Y) \to Y) & (SoA \ 2) \\ (11) & (Y) \to ((Y) \to Y) & (SoA \ 1) \\ (12) & ((Y) \to (((Y) \to Y) \to Y)) \to ((Y) \to Y) & (M.P. \ 11, 10) \\ (13) & (Y) \to (((Y) \to Y) \to Y) & (SoA \ 1) \\ (14) & (Y) \to Y & (M.P. \ 13, 12) \\ (15) & ((Y) \to Y) \to ((Y) \to Y \to X \wedge Y) \to ((Y) \to X \wedge Y) & (SoA \ 2) \\ (16) & ((Y) \to ((Y) \to X \wedge Y)) \to ((Y) \to X \wedge Y) & (M.P. \ 14, 15) \\ (17) & (Y) \to X \wedge Y & (M.P. \ 4, 1) \\ (18) & X \wedge Y \to Z & (Hyp. \ 1) \\ (19) & (X \wedge Y \to Z) \to ((Y) \to X \wedge Y \to Z) & (SoA \ 1) \\ (20) & (Y) \to X \wedge Y \to Z & (M.P. \ 18, 19) \\ (21) & ((Y) \to X \wedge Y) \to ((Y) \to X \wedge Y \to Z) \to ((Y) \to Z) & (SoA \ 2) \\ (22) & ((Y) \to ((X \wedge Y) \to Z)) \to ((Y) \to Z) & (M.P. \ 17, 21) \\ (23) & (Y) \to Z & (M.P. \ 20, 22) \\ \end{array}$$

[arseniiv]

Хорошо! (Надеюсь, вы не переписывали это всё вручную.) Только третий надо ещё раз модифицировать — чтобы получился вывод $X\wedge Y\to Z\vdash X\to Y\to Z$.

Теперь я могу показать уже преобразование второго правила Бернайса — ведь для него нужна только первая выводимость два раза. Правда, я её запишу сокращённо, но используя вашу нумерацию. (И ещё представим, что вместо шагов 19 и 31 гипотезу $X\to Y\to Z$ мы вводим самым первым шагом, который я обозначу $K_0$. Удобно, чтобы гипотеза использовалась всего раз и в самом начале.)

Итак, пускай в оригинальном выводе $\Gamma,\alpha\vdash\beta$ был кусок

$$\begin{array}{lll} a. & \varphi\to\psi & \ldots \\ a+1. & (\exists x.\;\varphi)\to\psi & \mathrm B_\exists, a \\ \end{array}$$

Тогда в преобразованном $\Gamma\vdash\alpha\to\beta$ будет следующий кусок:

$$\begin{array}{lll} K_0. & \alpha\to\varphi\to\psi & \ldots \\ K_1. & (\alpha\to\alpha\to\alpha)\to(\alpha\to(\alpha\to\alpha)\to\alpha)\to\alpha\to\alpha & A_2 \\ K_2. & \alpha\to\alpha\to\alpha & A_1 \\ & \cdots & \\ K_{52}. & (\varphi\to(\alpha\to\varphi\to\psi)\to\alpha\to\psi)\to(\varphi\to\alpha\to\psi) & \mathrm{MP}, K_{21}, K_{51} \\ K_{53}. & \varphi\to\alpha\to\psi & \mathrm{MP}, K_{50}, K_{52} \\ K'_0 & (\exists x.\;\varphi)\to\alpha\to\psi & B_\exists, K_{53} \\ K'_1. & (\Phi\to\Phi\to\Phi)\to(\Phi\to(\Phi\to\Phi)\to\Phi)\to\Phi\to\Phi & A_2 \\ K'_2. & (\exists x.\;\varphi)\to(\exists x.\;\varphi)\to(\exists x.\;\varphi) & A_1 \\ & \cdots & \\ K'_{52}. & (\alpha\to((\exists x.\;\varphi)\to\alpha\to\psi)\to(\exists x.\;\varphi)\to\psi)\to(\alpha\to(\exists x.\;\varphi)\to\psi) & \mathrm{MP}, K'_{21}, K'_{51} \\ K'_{53}. & \alpha\to(\exists x.\;\varphi)\to\psi & \mathrm{MP}, K'_{50}, K'_{52} \\ \end{array}$$

Здесь $\Phi\equiv\exists x.\;\varphi$ (сократил, потому что из-за длинной строки не влезал третий столбец). Вставляя ваш вывод $X\to Y\to Z\vdash Y\to X\to Z$ в первый раз, сделали замену $\alpha/X, \varphi/Y, \psi/Z$. Вставляя во второй раз, сделали $\exists x.\;\varphi/X, \alpha/Y, \psi/Z$. Что чем заменять, в точности определяется определёнными, когда нашли, что было применено правило Бернайса, подформулами и гипотезой, которую мы убираем в данном случае.

[Kosat]

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

P.S. Там нумерованный дважды модифицированный третий вообще на 71 строку.

[arseniiv]

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

(А можно возложить весь вывод на программу, см. ниже.) <…> В книге кусок вывода, соответствующий применению эквивалентности пропозициональных формул, опущен только из-за доказанной раньше теоремы о $\Gamma\vdash\varphi\Leftrightarrow\Gamma\vDash\varphi$ для исчисления высказываний, и конструирование вывода возложено на неё (и с ним справится в данном случае программа при любом корректном входе).

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

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

[Kosat]

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

В книге кусок вывода, соответствующий применению эквивалентности пропозициональных формул, опущен только из-за доказанной раньше теоремы о $\Gamma\vdash\varphi\Leftrightarrow\Gamma\vDash\varphi$ для исчисления высказываний, и конструирование вывода возложено на неё

Я отчасти вижу и понимаю ваше стремление (50/50), но всё-таки желателен более короткий метод. Подстановка в строку значений у меня не очень реализована, я стараюсь держать программу возможно более простой, без ничего лишнего.

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

Можете вот так сделать, посмотрев, как там в доказательстве теоремы из правого получается левое.

Слишком много повторяющегося кода получится. Здесь задействован весь спектр случаев - и гипотезы, и схемы аксиом, и modus ponens. Я всего лишь хочу скомпоновать выходную строку нужным образом, ничего особо не меняя в основной части программы...

[arseniiv]

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

Подстановка в строку значений у меня не очень реализована

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

Кстати, на каком языке пишете, если не секрет? (Правда, ничего полезного посоветовать не обещаю. )

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

Слишком много повторяющегося кода получится. Здесь задействован весь спектр случаев - и гипотезы, и схемы аксиом, и modus ponens.

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

Или сделать, но почему-то никто в эту тему не пишет и не опровергнет.

[Kosat]

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

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

Кстати, на каком языке пишете, если не секрет? (Правда, ничего полезного посоветовать не обещаю. )

Я делаю ПОЛИЗ. Пишу на С++.

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

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

Или сделать, но почему-то никто в эту тему не пишет и не опровергнет.

Я всё там добавляю вручную (в скобках можно запутаться; я хочу красиво). Несложные же на вид формулы - может и есть способ. Вы просто привыкли к теореме о дедукции. Мне надо лучше думать.