Выводимое Правило

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