Afsnit (bevisteori)

En cut in proof-teori er en slutningsregel, der giver dig mulighed for at fjerne (“udskille”) en mellemsætning : $EN$

{\cfrac {\ \Gamma \ \rightarrow \ \Delta ,\ A\qquad A,\ \Theta \ \rightarrow \ \Lambda \ }{\Gamma ,\ \Theta \ \rightarrow \ \Delta ,\ \ Lambda }}

Da sektionsreglen ikke har underformelegenskaben (kræver, at præmisserne består af konklusionens underformler), får logiske regnestykker med sektionsfjernbarhed særlig betydning (herunder for muligheden for konstruktivt at bevise deres konsistens ) , det vil sige dem, hvor evt. afledbar sekvent kan udledes uden sektioner. For den klassiske og intuitionistiske sekvensregning blev egenskaben bevist af Gentzen , senere blev den etableret for en stor række af klassiske og ikke-klassiske teorier om højere orden.

Litteratur

G. Takeuchi. Bevisteorien. - M . : Mir, 1978. - 412 s.
Underformelegenskaben er en artikel fra Encyclopedia of Mathematics . S. Yu. Maslov