Cálculo de secuentes

El cálculo de secuentes es, en esencia, un estilo de argumentación lógica formal donde cada línea de la demostración es una tautología condicional (llamada secuente por Gerhard Gentzen) en vez de una tautología no condicional. Cada tautología condicional se infiere de otras tautologías condicionales en líneas anteriores de la demostración, de acuerdo a reglas y procedimientos de inferencia, dando así una mejor aproximación al estilo de deducción natural utilizado por los matemáticos que el estilo de David Hilbert, donde cada línea era una tautología no condicional. Puede que haya distinciones más sutiles: por ejemplo, podría haber axiomas no lógicos sobre los que todas las proposiciones son implícitamente dependientes. Entonces los secuentes son teoremas condicionales en un lenguaje de primer orden, en vez de tautologías condicionales. * Datos: Q1771121