Практическое значение синтаксического определения теоремы как элемента множества, порождаемого дедуктивной системой, заключается в возможности доказательства любой теоремы компьютером с неограниченным временем работы. Одним из способов непосредственной реализации данной идеи является построение формальной грамматики дедуктивной системы. Так, при автоматическом доказательстве теорем методами машинного обучения в качестве обучающей выборки мы могли бы указать множество пар вида (X,Y), где X — теорема, а Y — порождающая X последовательность правил вывода формальной грамматики. В данной статье мы ограничимся построением грамматики исчисления высказываний. Полученная грамматика типа 0 иерархии Хомского порождает язык, словами которого являются все тавтологии.

Defined syntactically, a theorem is a word generated by a deductive system. In practice, this means that each theorem can be proven by a sufficiently long working computer. A possible implementation of this idea is based on the construction of a formal grammar of the deductive system. In automated theorem proving based on the machine learning, we then can use pairs (X,Y) as the training data, where X stands for a theorem and Y is a sequence of inference rules of the formal grammar corresponding to X. This article provides the formal grammar of propositional calculus, namely, type 0 grammar producing all tautologies.