Вывод теорем

[damir_777]

Здравствуйте. Хочу задать небольшой вопрос относительно вывода теорем в заданной формализации логики высказываний.
К примеру, пусть задана следующая формализация:
Аксиома 1 (А1):
$(F\to (G\to F))$
Aксиома 2 (А2):
$(F\to (G\to H))\to ((F\to G)\to (F\to H))$
Ну третью аксиому я приводить не буду, она сейчас не нужна. Используется два знака: Отрицание и Импликация. Правило вывода: Modus Ponens.
Необходимо доказать (вывести) что $F\to F$.
В учебнике приводится такой пример вывода:
В Аксиоме 2 (А2) F и G заменяются на F. a G на $F\to F$. Схема вывода такая:
1.$(F\to ((F\to F)\to F))\to ((F\to (F\to F))\to (F\to F))$ (A2)
2.$F\to ((F\to F)\to F)$ (A1, где G заменена на $F\to F$)
3.$(F\to (F\to F))\to (F\to F)$ (Modus Ponens к п.1 и п.2)
4.$F\to (F\to F)$ (A1, G заменена на F)
5.$F\to F$ (Modus Ponens к 3, 4)
А можно ли сделать так:
Вариант 1.
1.$(F\to (F\to F))\to ((F\to F)\to (F\to F))$ (A2, G и H заменены на F)
2.$F\to (F\to F)$ (A1, где G заменена на F)
3.$(F\to F)\to (F\to F)$ (Modus Ponens к п.1 и п.2)
4.$F\to F$ (A1, где $(G\to F)$ заменено на F)
5.$F\to F$ (Modus Ponens к 3, 4)
Правда вот в пункте 4 аксиома совпадает с теоремой. Незнаю, можно ли так. И вот еще один вариант:
Вариант 2.
1.$F\to (F\to F)$ (A1, где G заменена на F)
2.F (просто формула в данной формализации)
3.$F\to F$ (Modus Ponens к 1, 2)
Вот вообще в рамках данной формализации хотелось бы узнать, может есть какие нибудь алгоритмы которые сразу позволяют сделать нужные замены чтобы получить из теоремы выводы. т.е не подгонять и проверять каждую аксиому , а как бы сразу по какому то правилу подставлять в нужные аксиомы нужные замены чтобы получить вывод)

[whitefox]

damir_777 в сообщении #1100337 писал(а):

4.$F\to F$ (A1, где $(G\to F)$ заменено на F)

Тогда уж:
1.$F\to F$ (A1, где $(G\to F)$ заменено на $F$)

Так нельзя. Вместо переменной можно подставить любую формулу, но вместо формулы — нет.

-- 18 фев 2016, 11:59 --

damir_777 в сообщении #1100337 писал(а):

2.F (просто формула в данной формализации)

И так нельзя. Каждый пункт доказательства должен быть либо аксиомой, либо выведен из предыдущих пунктов.

[damir_777]

Аа..ну насчет второго варианта понял. Я просто подумал что раз в аксиомах используется символ "F" и он принят в данной формализации, то значит его можно использовать

[whitefox]

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

[damir_777]

да. да. точно. Забыл совсем, что это схема)
а вот что насчет алгоритмов. Есть ли что нибудь что облегчает вывод теорем?

[whitefox]

Правило резолюций вам в помощь.

-- 18 фев 2016, 12:36 --

Или почитайте:
Ч.Чень, Р.Ли Математическая логика и автоматическое доказательство теорем.

[arseniiv]

(Те, кто знают, знают, а кто не знает, не поймут, но вывод в конце для вторых примечателен.)

Вывести $A\to A$ из этих двух схем можно как угодно. При изоморфизме Карри—Говарда они соответствуют λ-комбинаторам $K, S$, а выводимая — комбинатору $I$, который можно выразить через них как $(SK)(\text{что угодно})$. Только для наших целей этому чему угодно должно быть можно приписать тип $a\to b$, а то выведется формула $\mathcal F\to\mathcal F$, где $\mathcal F$ — формула, не являющаяся переменной; λ-термов с таким типом из $S, K$ можно насобирать сколько угодно — годятся $SXY$, $KZ$ и $K$ для $X\colon a\to t\to u, Y\colon a\to t$, где $a$ — обязательно переменная, $Z$ любого типа. В частности, первое (и последнее) приведённое ТС классическое доказательство соответствует равенству $I = (SK)K$. Можно построить другое доказательство, соответствующее, скажем, $I = (SK)(KK)$ или $I = (SK)((S(KK))K)$, но они (и все остальные) будут длиннее. Пример с первым:

$\begin{array}{rll} 1.& (A \to (B \to C \to B) \to A) \to (A \to B \to C \to B) \to A \to A & (S) \\ 2.& A \to (B \to C \to B) \to A & (K) \\ 3.& (A \to B \to C \to B) \to A \to A & (SK = \mathrm{MP}\, 1, 2) \\ 4.& (B \to C \to B) \to A \to B \to C \to B & (K) \\ 5.& B \to C \to B & (K) \\ 6.& A \to B \to C \to B & (KK = \mathrm{MP}\, 4, 5) \\ 7.& A \to A & ((SK)(KK) = \mathrm{MP}\, 3, 6) \end{array}$

Где-то недавно я писал, что можно взять $(SK)S$, и был неправ по причине, указанной выше. Надеюсь, читавшие простят.