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

- метаматематическая теорема (см. Метатеорема), позволяющая по конечному числу выводов из гипотез [img: http://localhost:8080/file/010321-183.jpg] утверждать выводимость формулы [img: http://localhost:8080/file/010321-184.jpg] из гипотез Г; выводы [img: http://localhost:8080/file/010321-185.jpg] наз. вспомогательными выводами В. п., заключение [img: http://localhost:8080/file/010321-186.jpg] наз. результирующим выводом. В. п. является частным случаем допустимого правила. Важнейшие примеры В. п. доставляются дедукции теоремой, правилом приведения к абсурду и другими правилами введения и удаления логических символов, такими, как правила введения дизъюнкции: [img: http://localhost:8080/file/010321-187.jpg] и [img: http://localhost:8080/file/010321-188.jpg] (для этих В. п. число вспомогательных выводов равно нулю) и удаления дизъюнкции: из [img: http://localhost:8080/file/010321-189.jpg] и Г, [img: http://localhost:8080/file/010321-190.jpg] следует [img: http://localhost:8080/file/010321-191.jpg]. В ряде случаев В. п. имеют такую структуру: исчисление расширяется и усиливается, и из выводимости в новом исчислении извлекаются следствия о выводимости в исходном. -Такие В. п. возникают, в частности, при устранении описательных определений (определении, к-рые моделируют происходящее при построении математич. теорий расширение понятий и обозначений). Разработанный аппарат В. п. служит существенному приближению методов обращения с формальными выводами к содержательным математич. рассуждениям. С. ю. Маслов,