Русская Википедия:Сечение (теория доказательств)

Материал из Онлайн справочника
Перейти к навигацииПерейти к поиску

Шаблон:Значения Сечение в теории доказательств — правило вывода, позволяющее удалить («высечь») промежуточное высказывание <math>A</math>:

<math>\cfrac {\ \Gamma \ \rightarrow \ \Delta, \ A \qquad A, \ \Theta \ \rightarrow \ \Lambda \ }{\Gamma, \ \Theta \ \rightarrow \ \Delta, \ \Lambda }</math>.

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

Литература