posic | Матлогическое

Математики часто говорят, что некоторые два доказательства по существу одинаковы; иногда же два доказательства одного утверждения представляются существенно различными. Далее, можно себе представить, что математик не усматривает одинаковости двух доказательств, но готов пересмотреть свое мнение, если ему представят соображения, иллюстрирующие их эквивалентность (например, доказательство эквивалентности понятий, используемых в ходе первого и второго доказательства); обратное представить себе труднее. Наконец, вроде бы иногда имеет смысл говорить, что одно доказательство несет в себе больше информации, чем другое (скажем, опирается на более сильные леммы и доказывает по существу более сильное утверждение).

Знает ли наука матлогика понятие трансформаций логических выводов, которое формализовало бы это представление об одинаковых и разных доказательствах? Аналогичное понятие трансформаций алгоритмов и т.п. объектов? Другими словами, утверждения и доказательства в фиксированной аксиоматике образуют категорию (утверждения - объекты, выводы одних утверждений из других - морфизмы); нельзя ли вложить ее в естественную 2-категорию?