Avsnitt (bevisteori)

En nedskärning av bevisteori  är en slutledningsregel som gör att du kan ta bort (”skära ut”) ett mellanpåstående :

.

Eftersom sektionsregeln inte har delformelegenskapen (kräver att lokalerna består av underformler till slutsatsen), får logiska kalkyler med sektionsborttagningsbarhet särskild betydelse (inklusive för möjligheten att konstruktivt bevisa sin överensstämmelse ) , det vill säga de där ev. härledbar sekvens kan härledas utan sektioner. För den klassiska och intuitionistiska sekvenskalkylen bevisades egenskapen av Gentzen , senare etablerades den för en stor serie klassiska och icke-klassiska teorier om högre ordning.

Litteratur