Сечение (теория доказательств)

Материал из Википедии — свободной энциклопедии
Перейти к навигации Перейти к поиску

Сечение в теории доказательств — правило вывода, позволяющее удалить («высечь») промежуточное высказывание :

.

Поскольку правило сечения не обладает свойством подформульности (требующим, чтобы посылки состояли из подформул заключения), особую значимость (в том числе для возможности конструктивного доказательства их непротиворечивости) приобретают логические исчисления с устранимостью сечений, то есть такие, в которых всякую выводимую секвенцию можно вывести без сечения. Для классического и интуиционистского исчислений секвенций свойство доказано Генценом, в дальнейшем оно установлено для большой серии классических и неклассических теорий высших порядков.

Литература

[править | править код]
  • Г. Такеути. Теория доказательств. — М.: Мир, 1978. — 412 с.
  • Подформульности свойство — статья из Математической энциклопедии. С. Ю. Маслов