En la teoría de la prueba , una regla estructural es una regla de inferencia que no se refiere a ningún conectivo lógico , sino que opera directamente sobre el juicio o las secuencias . Las reglas estructurales a menudo imitan las propiedades metateóricas pretendidas de la lógica. Las lógicas que niegan una o más de las reglas estructurales se clasifican como lógicas subestructurales .
Una lógica sin ninguna de las reglas estructurales anteriores interpretaría los lados de un secuente como secuencias puras ; con intercambio, son multijuegos ; y tanto con contracción como con intercambio son conjuntos .
Éstas no son las únicas reglas estructurales posibles. Una famosa regla estructural se conoce como corte . Los teóricos de la prueba dedican un esfuerzo considerable a demostrar que las reglas de corte son superfluas en varias lógicas. Más precisamente, lo que se muestra es que cortar es solo (en cierto sentido) una herramienta para abreviar demostraciones y no se suma a los teoremas que pueden demostrarse. La "eliminación" exitosa de las reglas de corte, conocida como eliminación de cortes , está directamente relacionada con la filosofía del cálculo como normalización (ver correspondencia Curry-Howard ); a menudo da una buena indicación de la complejidad de decidir una lógica dada.