Teorema de cort-eliminació

La teorema de cort-eliminació (o Gentzen Hauptsatz) és una teorema que establix l'importància del càlcul de secuentes. Va ser demostrat per Gerhard Gentzen en 1934 en el seu artícul Investigacions sobre la deducció llògica per als sistemes LJ i LK formalisant la llògica intuicionista i la llògica clàssica, respectivament. La teorema de cort-eliminació establix que qualsevol demostració que tinga una demostració en el càlcul de secuentes i use la regla de tall, també té una demostració sense tall, és dir que no faça us de la regla de cort.