Сегодня, путешествуя между остановкой и домом, я вдруг задумался о том, как грамматикой задать некую схему аксиом, да к примеру хотя бы что-нибудь вроде
\rightarrow(A\rightarrow(B\rightarrow C))\rightarrow(A\rightarrow C))))
.
Пришёл к выводу, что задача на самом деле очень не простая, и идей, как это сделать, я не представляю - даже для простого случая
)
придумать адекватную схему замен не получается.
Проблему для себя я нашёл в том, что в данном случае несмотря на то, что из A, B и C (в простом случае A) можно по идее выводить любую формулу, в разных вхождениях формула должна выводиться одна и та же.
На всякий случай уточню правила для вывода формул, которые я использовал:
<br /><br />F \rightarrow(F \vee F)<br /><br />F\rightarrow (\forall x F)<br /><br />F\rightarrow (\exists x F)<br /><br />F \rightarrow \neg F<br /><br />F \rightarrow P_i(\overline{x}_{\nu(i)}).)
Вход
FAQ
Поиск
