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

[posic]

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

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

Comments

[siyuv.livejournal.com]

Возможно частичный ответ на этот вопрос находится здесь. Если удастся разобраться, то поделитесь пожалуйста.

[posic.livejournal.com]

Спасибо за ссылку.

[archernikov.livejournal.com]

Случайно наткнулся на ссылку, может быть вас заинтересует.
http://www.math.ucla.edu/~asl/bsl/1301/1301-006.ps
Там рецензия на некую книгу на подобную тему с несколькими ссылками, как раз в категорном контексте.

[posic.livejournal.com]

Спасибо. То есть, видимо, вопрос рассматривается, но пока что не вполне изучен.

[brshk.livejournal.com]

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