Un marco proof-teórico en el que las reglas de inferencia pueden aplicarse a cualquier profundidad dentro de expresiones lógicas en lugar de solo en la raíz; la inferencia profunda admite sistemas de prueba simétricos, locales y frecuentemente más compactos como el Calculus of Structures.

Principio

Permitir la aplicación de reglas dentro de subfórmulas arbitrarias: los contextos de inferencia no se limitan al nivel superior, lo que posibilita reescrituras locales que comprimen o simetrian la estructura de la prueba, siempre que se preserven propiedades meta (corrección, eliminación de cortes) mediante el diseño apropiado de reglas y controles estructurales.

Demostración

En un sistema de inferencia profunda para lógica proposicional, una regla que reemplaza A∨(B∧C) por (A∨B)∧(A∨C) puede aplicarse dentro de contextos mayores, p. ej. dentro de X[…], de modo que se reescribe una subfórmula anidada directamente sin elevarla al nivel superior; esta localidad puede producir derivaciones más cortas que los sistemas tipo sequent.

Aplicación incorrecta

Permitir de forma ingenua reescrituras internas arbitrarias sin restricciones puede romper terminación o corrección (derivaciones que entran en bucle o que producen secuencias inválidas); diseñar reglas profundas sin control en lógicas con comportamiento estructural complejo puede provocar no-confluencia o cortes no eliminables.

Consecuencia

La inferencia profunda suele dar lugar a pruebas más cortas y simétricas, soporta una localidad fina adecuada para la paralelización y posibilita sistemas uniformes para lógicas clásicas y no clásicas que resisten presentaciones compactas en sequent.

Inversión

El reverso es la inferencia superficial (sistemas tradicionales de sequent o deducción natural) donde las reglas actúan solo en el nivel más externo; los sistemas superficiales favorecen una lectura operativa clara y estrategias de normalización establecidas, pero pueden generar pruebas más largas y secuenciales.

Límite

Se aplica cuando los conectivos y las reglas estructurales permiten reescrituras internas locales y cuando se pueden imponer controles metateóricos; no es una panacea para todas las lógicas: algunos sistemas requieren restricciones estructurales adicionales o un aparato etiquetado para recuperar propiedades como la eliminación de cortes y la decidibilidad.

Tensión semántica

Existe tensión entre inferencia profunda y cálculos estilo sequent: la inferencia profunda enfatiza localidad y simetría a costa de una metateoría más compleja, mientras que los cálculos sequent ponen énfasis en la composición modular de reglas y normalizaciones más sencillas; ambas opciones negocian longitud de prueba, claridad y control proof-teórico.

Síntesis

La Inferencia Profunda generaliza dónde y cómo se aplican las reglas dentro de las fórmulas: al permitir reescrituras locales y profundas se obtienen sistemas de prueba compactos y simétricos que revelan paralelismo y modularidad, pero el enfoque exige diseño cuidadoso de reglas y restricciones estructurales para garantizar corrección y normalización.