2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему На страницу Пред.  1, 2, 3, 4
 
 Re: Как доказать общезначимое высказывание с помощью исчисления
Сообщение06.05.2015, 02:26 
Заслуженный участник


27/04/09
28128
Так, стоп, у вас уже есть программа, генерирующая вывод в соответствии с пропозициональной теоремой о дедукции? Если есть, так и загоните в неё
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 писал(а):
напишите выводы
Если забыл сказать, они пишутся почти что сами собой.

 Профиль  
                  
 
 Re: Как доказать общезначимое высказывание с помощью исчисления
Сообщение06.05.2015, 02:57 
Аватара пользователя


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

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

 Профиль  
                  
 
 Re: Как доказать общезначимое высказывание с помощью исчисления
Сообщение06.05.2015, 23:50 
Заслуженный участник


27/04/09
28128
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 писал(а):
Ваш длинный вывод вообще непонятно каким здесь боком.
Ну как же непонятно каким, когда самым прямым (см. выше)!

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

 Профиль  
                  
 
 Re: Как доказать общезначимое высказывание с помощью исчисления
Сообщение07.05.2015, 00:36 
Аватара пользователя


07/01/14
119
arseniiv в сообщении #1011914 писал(а):
Да, с нуля получить вывод в нашем случае уже нельзя для всякой формулы — для каких-то любой алгоритм не завершится.

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

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

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

 Профиль  
                  
 
 Re: Как доказать общезначимое высказывание с помощью исчисления
Сообщение07.05.2015, 08:14 
Заслуженный участник


27/04/09
28128

(Оффтоп)

Kosat в сообщении #1011933 писал(а):
Заставим. Надо только те пропозициональные тождества вывести.
Среди заданий вроде не было вывода произвольной формулы с нуля, вы ж и сами говорили.

Kosat в сообщении #1011933 писал(а):
Но мы сейчас пытаемся адаптировать ход доказательства теоремы о дедукции в исчислении предикатов к заданию номер четыре. Для этого нет другого пути, кроме как расписать пропущенные действия на с.142-143 в вашей книге.
Вот те пропущеные действия и есть шаги вставляемого-с-подстановкой вывода, в том-то и дело! :-) Чем они ещё могут быть? Применением какого-то одного неизвестного правила вывода — нам это не позволено.

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

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

 Профиль  
                  
 
 Re: Как доказать общезначимое высказывание с помощью исчисления
Сообщение07.05.2015, 10:36 
Аватара пользователя


07/01/14
119
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$. Получатся два вывода, вставляемые как раз в проиллюстрированном переписывании первого правила Бернайса.

 Профиль  
                  
 
 Re: Как доказать общезначимое высказывание с помощью исчисления
Сообщение09.05.2015, 01:07 
Заслуженный участник


27/04/09
28128
Kosat в сообщении #1012005 писал(а):
Вы в одном месте правильно указали требуемые пропозициональные тавтологии, в другом - преобразовали свой вывод на вывод после применения теоремы о дедукции. В одном месте говорите, что он поможет всё решить, в другом - что не можете обработать даже простые входные данные задания 4 (предварительно потребовав их от меня). Странно всё это.
Тут всё просто: те выводы, которые нужны, конструируются как-то не очень прозрачно — а вот эквивалентные им по т. о д. идут как по маслу. После чего применяем к такому прозрачному выводу прозрачную процедуру из теоремы — да, в результате получится монстр о десятках формул — но проверять корректность-то не человеку. Если мы напишем неправильный вывод, программа первой же скажет, что это не работает, так что сделать что-то неправильно таким способом нельзя. (А можно возложить весь вывод на программу, см. ниже.)

Kosat в сообщении #1012005 писал(а):
P.S. Я догадываюсь, что вы изобрели какой-то "универсальный метод" и тщетно пытаетесь мне растолковать его применение для первого правила Бернайса.
Вряд ли даже переизобрёл — просто сложил два и два. Уверен, через какое-то время и вам это станет более-менее очевидно. :-)

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

 Профиль  
                  
 
 Re: Как доказать общезначимое высказывание с помощью исчисления
Сообщение09.05.2015, 19:15 
Аватара пользователя


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

Нумерованный первоначальный первый:
$$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}$$

 Профиль  
                  
 
 Re: Как доказать общезначимое высказывание с помощью исчисления
Сообщение09.05.2015, 22:29 
Заслуженный участник


27/04/09
28128
Хорошо! :appl: (Надеюсь, вы не переписывали это всё вручную.) Только третий надо ещё раз модифицировать — чтобы получился вывод $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$. Что чем заменять, в точности определяется определёнными, когда нашли, что было применено правило Бернайса, подформулами и гипотезой, которую мы убираем в данном случае.

 Профиль  
                  
 
 Re: Как доказать общезначимое высказывание с помощью исчисления
Сообщение09.05.2015, 23:37 
Аватара пользователя


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

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

 Профиль  
                  
 
 Re: Как доказать общезначимое высказывание с помощью исчисления
Сообщение09.05.2015, 23:42 
Заслуженный участник


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

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

 Профиль  
                  
 
 Re: Как доказать общезначимое высказывание с помощью исчисления
Сообщение10.05.2015, 00:29 
Аватара пользователя


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

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

arseniiv в сообщении #1012968 писал(а):
Можете вот так сделать, посмотрев, как там в доказательстве теоремы из правого получается левое.

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

 Профиль  
                  
 
 Re: Как доказать общезначимое высказывание с помощью исчисления
Сообщение10.05.2015, 01:00 
Заслуженный участник


27/04/09
28128
Kosat в сообщении #1012999 писал(а):
Подстановка в строку значений у меня не очень реализована
А вы, получается, не делаете дерева выражения? Мне казалось, для использования правил вывода без этого практически никак. Простота в программе, манипулирующей формулами и выводами как раз в разборе строк и работе с более подходящим представлением.

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

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

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

 Профиль  
                  
 
 Re: Как доказать общезначимое высказывание с помощью исчисления
Сообщение10.05.2015, 01:16 
Аватара пользователя


07/01/14
119
arseniiv в сообщении #1013019 писал(а):
А вы, получается, не делаете дерева выражения? Мне казалось, для использования правил вывода без этого практически никак. Простота в программе, манипулирующей формулами и выводами как раз в разборе строк и работе с более подходящим представлением.

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

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

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

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

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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 59 ]  На страницу Пред.  1, 2, 3, 4

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: YandexBot [bot]


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

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group