Здравствуйте. Хочу задать небольшой вопрос относительно вывода теорем в заданной формализации логики высказываний.
К примеру, пусть задана следующая формализация:
Аксиома 1 (А1):
![$(F\to (G\to F))$ $(F\to (G\to F))$](https://dxdy-01.korotkov.co.uk/f/c/1/4/c1467be53829ac961cbb2d1fa6abc3d082.png)
Aксиома 2 (А2):
![$(F\to (G\to H))\to ((F\to G)\to (F\to H))$ $(F\to (G\to H))\to ((F\to G)\to (F\to H))$](https://dxdy-03.korotkov.co.uk/f/a/1/3/a131195064cdf94d7a6f46eec7b734bf82.png)
Ну третью аксиому я приводить не буду, она сейчас не нужна. Используется два знака: Отрицание и Импликация. Правило вывода: Modus Ponens.
Необходимо доказать (вывести) что
![$F\to F$ $F\to F$](https://dxdy-01.korotkov.co.uk/f/0/0/a/00acebc6ce2d09b3c37a68ad85e8836c82.png)
.
В учебнике приводится такой пример вывода:
В Аксиоме 2 (А2) F и G заменяются на F. a G на
![$F\to F$ $F\to F$](https://dxdy-01.korotkov.co.uk/f/0/0/a/00acebc6ce2d09b3c37a68ad85e8836c82.png)
. Схема вывода такая:
1.
![$(F\to ((F\to F)\to F))\to ((F\to (F\to F))\to (F\to F))$ $(F\to ((F\to F)\to F))\to ((F\to (F\to F))\to (F\to F))$](https://dxdy-04.korotkov.co.uk/f/f/6/b/f6b2652e634ff8d78b4b7c22a15a8ca882.png)
(A2)
2.
![$F\to ((F\to F)\to F)$ $F\to ((F\to F)\to F)$](https://dxdy-01.korotkov.co.uk/f/c/4/8/c4813b0f520ae278e3b3c9a7e0f8117182.png)
(A1, где G заменена на
![$F\to F$ $F\to F$](https://dxdy-01.korotkov.co.uk/f/0/0/a/00acebc6ce2d09b3c37a68ad85e8836c82.png)
)
3.
![$(F\to (F\to F))\to (F\to F)$ $(F\to (F\to F))\to (F\to F)$](https://dxdy-02.korotkov.co.uk/f/d/e/7/de76d07d0ae2520aa59e2b2917ee5fc282.png)
(Modus Ponens к п.1 и п.2)
4.
![$F\to (F\to F)$ $F\to (F\to F)$](https://dxdy-02.korotkov.co.uk/f/d/5/5/d5582e85ad66b85a992d69ac663a84ce82.png)
(A1, G заменена на F)
5.
![$F\to F$ $F\to F$](https://dxdy-01.korotkov.co.uk/f/0/0/a/00acebc6ce2d09b3c37a68ad85e8836c82.png)
(Modus Ponens к 3, 4)
А можно ли сделать так:
Вариант 1.
1.
![$(F\to (F\to F))\to ((F\to F)\to (F\to F))$ $(F\to (F\to F))\to ((F\to F)\to (F\to F))$](https://dxdy-02.korotkov.co.uk/f/5/6/4/564b94001ebee2dd13772574dd014ba282.png)
(A2, G и H заменены на F)
2.
![$F\to (F\to F)$ $F\to (F\to F)$](https://dxdy-02.korotkov.co.uk/f/d/5/5/d5582e85ad66b85a992d69ac663a84ce82.png)
(A1, где G заменена на F)
3.
![$(F\to F)\to (F\to F)$ $(F\to F)\to (F\to F)$](https://dxdy-01.korotkov.co.uk/f/0/3/0/03021be508db4f9598b4400aa3a7e71782.png)
(Modus Ponens к п.1 и п.2)
4.
![$F\to F$ $F\to F$](https://dxdy-01.korotkov.co.uk/f/0/0/a/00acebc6ce2d09b3c37a68ad85e8836c82.png)
(A1, где
![$(G\to F)$ $(G\to F)$](https://dxdy-04.korotkov.co.uk/f/3/a/c/3ac0500ac7259218dea704bf048ff53182.png)
заменено на F)
5.
![$F\to F$ $F\to F$](https://dxdy-01.korotkov.co.uk/f/0/0/a/00acebc6ce2d09b3c37a68ad85e8836c82.png)
(Modus Ponens к 3, 4)
Правда вот в пункте 4 аксиома совпадает с теоремой. Незнаю, можно ли так. И вот еще один вариант:
Вариант 2.
1.
![$F\to (F\to F)$ $F\to (F\to F)$](https://dxdy-02.korotkov.co.uk/f/d/5/5/d5582e85ad66b85a992d69ac663a84ce82.png)
(A1, где G заменена на F)
2.F (просто формула в данной формализации)
3.
![$F\to F$ $F\to F$](https://dxdy-01.korotkov.co.uk/f/0/0/a/00acebc6ce2d09b3c37a68ad85e8836c82.png)
(Modus Ponens к 1, 2)
Вот вообще в рамках данной формализации хотелось бы узнать, может есть какие нибудь алгоритмы которые сразу позволяют сделать нужные замены чтобы получить из теоремы выводы. т.е не подгонять и проверять каждую аксиому , а как бы сразу по какому то правилу подставлять в нужные аксиомы нужные замены чтобы получить вывод)