Статья 243

Можно построить для второпорядкового языка точную семантику и точным образом определить семантические понятия общезначимости и логического следования. Но при этом оказывается, что данные понятия в принципе не могут быть формализованы, нельзя построить такое обладающее свойством полноты непротиворечивое исчисление, в котором все правила вывода были бы финитны, а число логических аксиом конечным и рекурсивным. Строгое доказательство того, что семантическое понятие логического следования для второпорядкового языка принципиально не может быть формализовано в исчислении, было дано также К. Геделем в 1931 г. в его знаменитой работе О формальной неразрешимости предложений и родственных систем.
Логическое правило называется финитным, если число посылок этого правила конечно. Очевидно, что правила исчисления НС финитны. Часто упомянутый результат К.