Ну я и говорю: Вы пользуетесь коммутативностью дизъюнкции, но у нас она разве есть? У нас же ничего кроме MP, теоремы дедукции, аксиом и 9 секвенций нету. Впрочем, у нас есть секвенции 6 и 7, но тогда надо попытаться применить их предварительно.
или это неправильно?
Кстати, знака
![$\Leftrightarrow$ $\Leftrightarrow$](https://dxdy-02.korotkov.co.uk/f/9/7/6/976a30a7c71e849ba05370616ae73a9b82.png)
в ИВ тоже нет (т.е. в выводе его не должно быть). В ИВ формула
![$A\vee B$ $A\vee B$](https://dxdy-01.korotkov.co.uk/f/4/e/f/4ef8bbb924df876bc1dc66378948866782.png)
- это просто обозначение
![$\neg A\to B$ $\neg A\to B$](https://dxdy-03.korotkov.co.uk/f/2/5/7/25764548064c6b1d828e15b315f8472d82.png)
, причем никаких свойств этого обозначения мы не знаем (хотя они есть). Если мы какие-то его свойства хотим использовать, то их доказать нужно.
то есть правильно я понимаю:
![$(A\to B) \vdash (\neg B \to ( \neg C \to (A \to C)))$ $(A\to B) \vdash (\neg B \to ( \neg C \to (A \to C)))$](https://dxdy-02.korotkov.co.uk/f/9/9/a/99ad7b1d098b2c28b7b0b5a02447312f82.png)
![$\neg B \vdash (\neg C \to (A \to C))$ $\neg B \vdash (\neg C \to (A \to C))$](https://dxdy-04.korotkov.co.uk/f/3/e/7/3e751a68d0841fff052b2fcc7d33ef2482.png)
Если Вы до 1-й формулы дойдете (пока явно не дошли), то не так: у Вас 1-я гипотеза слева пропала, должно получиться две гипотезы:
![$(A\to B) \vdash (\neg B \to ( \neg C \to (A \to C)))$ $(A\to B) \vdash (\neg B \to ( \neg C \to (A \to C)))$](https://dxdy-02.korotkov.co.uk/f/9/9/a/99ad7b1d098b2c28b7b0b5a02447312f82.png)
выводимо тогда и только тогда, когда выводимо
![$(A\to B), \neg B \vdash \neg C \to (A \to C)$ $(A\to B), \neg B \vdash \neg C \to (A \to C)$](https://dxdy-03.korotkov.co.uk/f/6/2/2/622607758e4cb796b4c61cf8fba1dcaf82.png)
. Опять же, если до исходной точки дойдем, то можем применить теорему дедукции уже 3-й раз.