История изменений

поэтому рассуждения насчет категории формул и дедукций я чёт ниочинь

Это по Lambek-у (google://deductive+system+category — http://plato.stanford.edu/entries/category-theory, например). Из Mann «The connection between equivalence of proofs and Cartesian closed categories»:

there is in a cartesian closed category a terminal object, which must be represented by a formula in the formal system. The equivalence relation must allow for the fact that there is exactly one morphism into the terminal object from any other object. This terminal object is akin to a formula representing 'truth', which can be proved in essentially only one way.

про аксиомы как раз, такие как

------- (tt)
⊤ holds

----------- (refl)
x = x holds

То есть аксиомы — тривиальные теоремы, их доказательства — тривиальны, всё это терминальный объект и стрелки в него (там класс эквивалентности доказательств). Просто чтобы навести мосты с понятием «тривиально» из алгебры. Теперь из аксиом производим множество теорем исключительно «вычислительными» правилами вывода, суть в том, что такой вывод может быть однозначен и разрешим (Church–Rosser и нормализация), дальше добавляем весь класс таких теорем в класс очевидно-тривиальных аксиом, например

...
-------------------
2 + 3 = 3 + 2 holds

...
-------------------- (+0)
a |- 0 + a = a holds

...
--------------------------------------- (+1)
a, b |- (1 + a) + b = 1 + (a + b) holds

и считаем их тоже тривиальными. Это уже чтобы упростить доказательства «нетривиальных» вещей — современная теория типов (с учётом computational rules) и её реализации в пруф-ассистентах так делают — поэтому там 2 + 3 = 3 + 2 так же тривиально как и 5 = 5, вычислительное доказательство производится тайпчекером за ширмой, так же в случае 0 + a = a, (1 + a) + b = 1 + (a + b) и любых других распостранений бета-эквивалентностей задаваемых определениями функций.

Это одно и то же?

У Бурбаки есть такая сентенция:

Математик, желающий убедиться в полной правильности, или, как говорят, “строгости", доказательства или теории, отнюдь не прибегает к одной из тех полных формализаций, которыми мы сейчас располагаем, и даже большей частью не пользуется частичными и неполными формализациями, доставляемыми алгебраическим и другими подобными исчислениями. Обыкновенно он довольствуется тем, что приводит изложение к такому состоянию, когда его опыт и чутье математика говорят ему, что перевод на формализованный язык был бы теперь лишь упражнением в терпении. Если возникают сомнения, то, в конечном счете они относятся именно к возможности прийти без двусмысленности к такой формализации — употреблялось ли одно и то же слово в разных смыслах в зависимости от контекста, нарушались ли правила синтаксиса бессознательным употреблением способов рассуждения, не разрешаемых явно этими правилами, была ли, наконец, совершена фактическая ошибка. Текст редактируется, все больше и больше приближаясь к формализованному тексту, пока, по мнению специалистов, дальнейшее продолжение этой работы не станет излишним.

Правда в случае пруф-ассистентов остановиться уже нельзя — нужно формализировать до победного.

для языка, на котором они формулируются, не существует правил вывода, чтоб на вход - аксиомы и правила, и на выходе бесконечно выплевываются теоремы?

В смысле для естественного языка? Всё равно есть некоторое строгое представление о вещах в голове которые этим языком описываются — начиная с Евклида, плюс сейчас часто коммутативные и прочие диаграммы используются, явный equational reasoning, то есть когда вместо словесного описания выписываются шаги вывода и промежуточные результаты.

поэтому рассуждения насчет категории формул и дедукций я чёт ниочинь

Это по Lambek-у (google://deductive+system+category — http://plato.stanford.edu/entries/category-theory, например). Из Mann «The connection between equivalence of proofs and Cartesian closed categories»:

there is in a cartesian closed category a terminal object, which must be represented by a formula in the formal system. The equivalence relation must allow for the fact that there is exactly one morphism into the terminal object from any other object. This terminal object is akin to a formula representing 'truth', which can be proved in essentially only one way.

про аксиомы как раз, такие как

------- (tt)
⊤ holds

----------- (refl)
x = x holds

То есть аксиомы — тривиальные теоремы, их доказательства — тривиальны, всё это терминальный объект и стрелки в него (там класс эквивалентности доказательств). Просто чтобы навести мосты с понятием «тривиально» из алгебры. Теперь из аксиом производим множество теорем исключительно «вычислительными» правилами вывода, суть в том, что такой вывод может быть однозначен и разрешим (Church–Rosser и нормализация), дальше добавляем весь класс таких теорем в класс очевидно-тривиальных аксиом, например

...
-------------------
2 + 3 = 3 + 2 holds

...
-------------------- (+0)
a |- 0 + a = a holds

...
--------------------------------------- (+1)
a, b |- (1 + a) + b = 1 + (a + b) holds

и считаем их тоже тривиальными. Это уже чтобы упростить доказательства «нетривиальных» вещей — современная теория типов (с учётом computational rules) и её реализации в пруф-ассистентах так делают — поэтому там 2 + 3 = 3 + 2 так же тривиально как и 5 = 5, вычислительное доказательство производится тайпчекером за ширмой, так же в случае 0 + a = a, (1 + a) + b = 1 + (a + b) и любых других распостранений бета-эквивалентностей задаваемых определениями функций.

Это одно и то же?

У Бурбаки есть такая сентенция:

Математик, желающий убедиться в полной правильности, или, как говорят, “строгости", доказательства или теории, отнюдь не прибегает к одной из тех полных формализаций, которыми мы сейчас располагаем, и даже большей частью не пользуется частичными и неполными формализациями, доставляемыми алгебраическим и другими подобными исчислениями. Обыкновенно он довольствуется тем, что приводит изложение к такому состоянию, когда его опыт и чутье математика говорят ему, что перевод на формализованный язык был бы теперь лишь упражнением в терпении. Если возникают сомнения, то, в конечном счете они относятся именно к возможности прийти без двусмысленности к такой формализации — употреблялось ли одно и то же слово в разных смыслах в зависимости от контекста, нарушались ли правила синтаксиса бессознательным употреблением способов рассуждения, не разрешаемых явно этими правилами, была ли, наконец, совершена фактическая ошибка. Текст редактируется, все больше и больше приближаясь к формализованному тексту, пока, по мнению специалистов, дальнейшее продолжение этой работы не станет излишним.

Правда в случае пруф-ассистентов остановиться уже нельзя — нужно формализировать до победного.

для языка, на котором они формулируются, не существует правил вывода, чтоб на вход - аксиомы и правила, и на выходе бесконечно выплевываются теоремы?

В смысле для естественного языка? Всё равно есть некоторое строгое представление о вещах в голове которые этим языком описываются — начиная с Евклида, плюс сейчас часто коммутативные и прочие диаграммы используются, явный equational reasoning, то есть когда вместо словесного описания выписываются шаги вывода и промежуточные результаты.