Gentzenscher Hauptsatz

Der Gentzensche Hauptsatz oder Schnittsatz (englisch cut-elimination theorem) ist ein Satz der mathematischen Logik, der besagt, dass die Schnittregel in jeder Herleitung eines Gentzentypkalküls eliminierbar und damit zulässig ist. Er ist nach Gerhard Gentzen benannt, der ihn 1934 aufstellte und bewies.

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.