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.

1. ↑ Gentzen: Untersuchung über das logische Schließen. In: Mathematische Zeitschrift 39, 1934, 176–210.