Здравствуйте!
У меня два замечания к главе про логику.
I. В учебнике в главах 15.1 и 15.3 по сути изложен один и тот же натуральный вывод, просто в разных формах.
В современной литературе по логике можно встретить два (как минимум, я больше не встречал) способа изложения натурального вывода - традиционный в виде деревьев формул, и в форме секвенций. Второй вид очень похож на интуиционистское секвенциальное исчисление, их даже легко спутать, но это совершенно разные вещи. Проще всего различить их можно по структуре правил:
1) в натуральном выводе связки добавляются и удаляются из сукцедента. Правила так и называются "правило введения (или удаления) такой-то связки".
2) в секвенциальном исчислении (инт. и класс.) связки добавляются как в антецедент, так и в сукцедент. Правила называются "правило введения такой-то связки в антецедент (или сукцедент)". Для удаления связок можно использовать те же правила, но в обратную сторону. В этом смысле секвенциальное исчисление гораздо более симметрично, чем натуральный вывод. Именно стремление достичь этой симметрии и привело к рождению секвенциальных исчислений (тут по-хорошему я должен дать ссылку на работу Генцена, в которой он подробно излагает эту интуицию, но мне лень искать точное место
)
II. В главе 15.4 изложенный специальный вывод очень-очень близок к интуиционистскому Гильбертовскому исчислению высказываний, а именно: тут смешаны в одну кучу аксиомы и понятие вывода из гипотез. Незначительным формальными преобразованиями можно их разделить и получить Гильбертовское исчисление как оно есть.
Откровенно говоря, я впервые здесь встретил такое специальное исчисление, поэтому у меня нет четкого понимания, почему специальное исчисление лучше подходит для изложения введения в BiCCC. BiCCC знаю плохо. Я более-менее знаком с алгебрами Гейтинга, тут мне мой опыт и интуиция подсказывает, что Гильберт подходит лучше. Поэтому я не понимаю, зачем усложнять жизнь и вводить специальное исчисление.