Regra do corte

Em lógica matemática, a regra do corte é uma regra de inferência do cálculo de sequentes. É uma generalização da regra de inferência clássica modus ponens. Seu significado é o de que, se uma fórmula A é apresentada como uma conclusão em uma prova e como uma hipótese em outra prova, então uma terceira prova em que a fórmula A não aparece pode ser deduzida. No caso particular do modus ponens, por exemplo, as ocorrências de homem são eliminadas de Todo homem é mortal, Sócrates é um homem para se deduzir Sócrates é mortal.

Notação formal

Notação formal na notação do cálculo de sequentes :

corte

${\cfrac {\Gamma \vdash A,\Delta \qquad \Gamma ',A\vdash \Delta '}{\Gamma ,\Gamma '\vdash \Delta ,\Delta '}}$

Eliminação

A regra do corte é o tema de um importante teorema, o teorema da eliminação do corte. Ele afirma que qualquer sentença que possui uma prova dentro do cálculo de sequentes e que faça uso da regra do corte, também possui uma prova em que não se faz uso desta regra.