Что за логическая система

[Sonic86]

В книжке Лорьера Системы искусственного интеллекта гл. 9.3.1. проводится следующая логическая система. Я не знаю ее названия и кто автор и где об этом почитать - в этом вопрос.
Похоже на исчисление высказываний: в теории язык - пропозициональные переменные, связки $\supset$ - импликация и $\wedge$ - конъюнкция. Модус поненс $p,p\supset q \to q$ - это метатеорема, здесь запятая $,$ и $\to$ - аналоги $\wedge$ и $\supset$. Другая метатеорема, выводимая с помощью модус поненс и правила подстановки - $P\supset (Q\supset R)\to Q\supset (P\supset R)$. Далее, очень удобным средством для создания метатеорем являются метаметатеоремы. Например, такова метаметатеорема "если из $a$ можно вывести $b$ и из $b$ можно вывести $c$, то из $a$ можно вывести $c$". Для записи метаметатеорем автор использует точку с запятой $;$ и какой-то кружочек со стрелочкой типа $\circ\to$ - не знаю, как его писать - снова аналоги конъюнкции и импликации. И потом еще рассматривает метаметаметатеорему "если $a,b\to c$ - метатеорема, то $a\circ\to b\to c$" - метаметатеорема и говорит, что это метаметаметатеорема универсальной пригодности (интересно, что понимается под универсальной пригодностью? и вообще - разве $k$-метатеоремы позволяют перепрыгивать с метаутверждений одного порядка на метаутверждения другого порядка? )

Вот где это можно нормально прочитать? В списке литературы как-то не смог найти... Написано, что из этого Ж. Питр составил программу.
Еще: последняя 3-метатеорема странная - она связывает 1-метатеорему и 2-метатеорему - перепрыгивает через метауровни. А почему не обозначить все связки $\wedge_n$ и $\supset_n$ для $n\in\mathbb{N}$ и не утверждать, например, что если $p\wedge_n (p\supset_n q)\supset_n q$, то $P\wedge_{n+1} (P\supset_{n+1} Q)\supset_{n+1} Q$? (или последнее утверждение вообще не является $k$-метатеоремой для любого $k$?). В общем очень интересно и ничего не понимаю