Odnímatelnost sekcí

Odstranitelnost sekcí ( Gentzenův teorém , eliminační teorém ) je vlastnost logického kalkulu, podle které lze odvodit libovolnou sekvenční odvoditelnou v daném kalkulu bez použití pravidla sekce [1] . Hraje zásadní roli v teorii důkazů a důležitou metodologickou roli v matematické logice obecně vzhledem k tomu, že poskytuje konstruktivní metodu pro dokazování konzistence , zejména pro klasické a intuicionistické logiky prvního řádu [2] .

Pro klasický a intuicionistický sekvenční kalkul byla vlastnost prokázána Gentzenem v roce 1934 . V roce 1953 byla vyslovena Takeuchiho domněnka , podle níž odnímatelnost úseků probíhá pro jednoduchou teorii typů a jí odpovídající logiky vyššího řádu, později byla potvrzena - pro klasickou logiku druhého řádu odnímatelnost sekce dokázal Tate , pro jednoduchou teorii typů - Takahashi a Pravitsa byly brzy nalezeny důkazy pro řadu neklasických teorií vyššího řádu ( Dragalin ) a pokročilých teorií typů ( Girard pro systém F ).

Symbolická formulace: nechť a  být prokazatelné následnosti kalkulu ; jestliže  je počet následný , pak je prokazatelný [3] .

Poznámky

  1. ↑ Teorie důkazů, 1978 , s. 29.
  2. ↑ P. I. Bystrov. Eliminační teorém  // Nová filozofická encyklopedie  : ve 4 svazcích  / předchozí. vědecky vyd. rada V. S. Stepina . — 2. vyd., opraveno. a doplňkové - M .  : Myšlenka , 2010. - 2816 s.
  3. ↑ Ershov, 1987 , s. 214.

Literatura