Статья 501

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