Secțiunea (teoria dovezilor)

O teorie de reducere a probei  este o regulă de inferență care vă permite să eliminați („taie”) o afirmație intermediară :

.

Întrucât regula secțiunii nu are proprietatea de subformula (cerând ca premisele să fie formate din subformule ale concluziei), calculele logice cu amovibilitate de secțiune capătă o semnificație deosebită (inclusiv pentru posibilitatea de a demonstra constructiv consistența lor ) , adică acelea în care orice secvența derivabilă poate fi dedusă fără secțiuni. Pentru calculul secvențial clasic și intuiționist , proprietatea a fost dovedită de Gentzen , ulterior a fost stabilită pentru o serie mare de teorii clasice și neclasice de ordin superior.

Literatură