Статья 246

Выявление указанных или каких-то других свойств выводов особенно существенно в том случае, когда дело касается внелогических приложений формального исчисления. Разумеется, речь идет не только о чисто синтаксической стороне исчисления - о свойствах выводов как синтаксических объектов, не менее важны естественность, ясность, а возможно, какие-то другие свойства семантических построений, необходимые для более эффективного кодирования информации о той области объектов, о которой ведутся рассуждения.
Нетрудно убедиться, что с некоторой практической точки зрения исчисление гильбертовского типа весьма неудобно. Построение вывода в НС оказывается процедурой весьма неестественной и сложной, требующей определенных навыков и приложения творческих усилий. Причина заключается в том, что шаги построения вывода в аксиоматическом исчислении очень мелки.