ВЫВОДИМОЕ ПРАВИЛО

ВЫВОДИМОЕ ПРАВИЛО - метаматематическая теорема (см. Метатеорема), позволяющая по конечному числу выводов из гипотез Г_i ⊢ Δ_i(1 ≤ i ≤ n, n ≥ 0) утверждать выводимость формулы Δ из гипотез Г; выводы Г_i ⊢ Δ_i наз. вспомогательными выводами В. п., заключение Г ⊢ Δ наз. результирующим выводом. В. п. является частным случаем допустимого правила. Важнейшие примеры В. п. доставляются дедукции теоремой, правилом приведения к абсурду и другими правилами введения и удаления логических символов, такими, как правила введения дизъюнкции: A ⊢ А ∨ В и В ⊢ А ∨ В (для этих В. п. число вспомогательных выводов равно нулю) и удаления дизъюнкции: из Г, A ⊢ С и Г, B ⊢ С следует Г, A ∨ B ⊢ С. В ряде случаев В. п. имеют такую структуру: исчисление расширяется и усиливается, и из выводимости в новом исчислении извлекаются следствия о выводимости в исходном. Такие В. п. возникают, в частности, при устранении описательных определений (определений, к-рые моделируют происходящее при построении математич. теорий расширение понятий и обозначений). Разработанный аппарат В. п. служит существенному приближению методов обращения с формальными выводами к содержательным математич. рассуждениям.

С. Ю. Маслов.

Источники:

1. Математическая Энциклопедия. Т. 1 (А - Г). Ред. коллегия: И. М. Виноградов (глав ред) [и др.] - М., «Советская Энциклопедия», 1977, 1152 стб. с илл.