Cтраница 2
Кроме того, это определение довольно далеко от основных идой формализации. Оно основано на интуитивных интерпретациях формул формализованных языков, а не на непосредственном определении этих формул. Поэтому можно ожидать, что существует другое эквивалентное определение операции присоединения следствий, основанное только на синтаксических свойствах формул, понимаемых как конечные последовательности знаков. [16]
Кроме того, это определение довольно далеко от основных идей формализации. Оно основано на интуитивных интерпретациях формул формализованных языков, а не на непосредственном определении этих формул. Поэтому можно ожидать, что существует другое эквивалентное определение операции присоединения следствий, основанное только на синтаксических свойствах формул, понимаемых как конечные последовательности знаков. [17]
Однако для того, чтсбы проверить, является ли данная формула р заключением из данных посылок по одному из правил ( п) - ( ге), интерпретации совсем не нужны. Более того, эта проверка чрезвычайно проста: во всех правилах ( п) - ( ге) заключение получается из посылок с помощью простых операций над формулами, понимаемыми как конечные последовательности знаков. Этот синтаксический характер и простота практически требуются от всех правил вывода, принимаемых в формализованных языках. [18]
Однако для того, чтобы проверить, является ли данная формула р заключением из данных посылок по одному из правил ( п) - ( ге), интерпретации совсем не нужны. Более того, эта проверка чрезвычайно проста: во всех правилах ( п) - ( ге) заключение получается из посылок с помощью простых операций над формулами, понимаемыми как конечные последовательности знаков. [19]