3.9. Программа Ж. Питра для исчисления высказываний
3.9.1. Иерархия метатеорий
Теорема представляет собой высказывание в некоторой формальной системе. Метатеорема является высказыванием о теоремах формальной системы и представляет двойной интерес.
Рис. 3.21. Дерево поиска (а) и линейный вывод (б).
С одной стороны, она позволяет сократить доказательства, избегая повторения классических промежуточных этапов и, более того, выполняя непосредственный переход от спуска по дереву (рис. 3.21, а). С другой стороны, метатеорема позволяет осуществить наилучший глобальный обзор поиска и сконцентрировать внимание на наиболее важных направлениях, не загружая память несущественными результатами.
Манипуляции с мататеоремами могут осуществляться с помощью формальной системы второго по отношению к исходному уровня. При этом необходимо использовать обозначения, отличающиеся от обозначений исходной системы для новых операторов. Так, модус поненс является правилом вывода, которое позволяет порождать теоремы и, следовательно, является также. метатеоремой. Эта метатеорема может быть записана следующим образом:
т. е. если 
есть теорема и если 
есть теорема, то и 
является теоремой. Здесь запятая и стрелка являются соответствующими аналогами в метаязыке для символов А и 
и языка исходной системы.
Метатеоремы могут быть доказиы в рамках исходной формальной системы. Так, мы уже доказали выше, что 
исчислении высказываний из всякой теоремы вида
можно вывести (используя правило модус поненс и подстановки) новую теорему
Этот результат, являющийся метатеоремой в исчислении высказываний и записываемый в виде
применим ко многим выражениям исчисления высказываний. Отметим, что удобным средством для создания метатеорем является использование в этих целях мета-метатеорем.
Например, высказывание «если из а можно вывести b и если из 
можно вывести с, то можно вывести с из 
является мета-метатеоремой, которая выражает транзитивность дедукции. (Это свойство является очень ценным в фундаментальных теориях). Чтобы это отразить, в записи для импликации и конъюнкции в метаязыке будем использовать новые символы 
Тогда предыдущая мета-метатеорема, о транзитивности дедукции запишется следующим образом:
Вполне логично для таких порождающих мета-метатеорем, широко используемых математиками, создать некую общую программу. К сожалению, существуют важные мета-метатеоремы, применяемые только в какой-то данной формальной системе. Так, например, мета-метатеорема
не является теоремой во всех формальных логических теориях. Действительно, нужно внести особый оператор самого языка — символ 
который не обязательно существует во всех теориях.
В общем случае все мета-метатеоремы, в которых фигурируют операторы исходной формальной системы, являются узко специальными. Необходимо, следовательно, создать какое-то средство для доказательства мета-метатеорем. Для этого определяют мета-мета-метатеорию. На этом уровне достигается уже такая степень общности, которая сегодня достаточна для всех областей математики. Таким образом, выражение Если
является метатеоремой, то 
является метаметатеоремой" представляет собой мета-мета-метатеорему универсальной пригодности.
