Un cálculo estructural de pruebas caracterizado por postulados de display que permiten 'exhibir' (aislar) cualquier subestructura de un sequent en un lado del símbolo de juicio para que se aplique la regla principal; la lógica de display proporciona un mecanismo uniforme para manejar conectivos diversos y manipulaciones estructurales.

Principio

Usar conectivos estructurales y postulados de display para reordenar sequents de modo que cualquier subestructura elegida pueda moverse a la posición focal; una vez exhibida, las reglas lógicas se aplican localmente a esa subestructura y teoremas meta como la eliminación de cortes se derivan de la gestión uniforme de la estructura.

Demostración

Para aplicar una regla de implicación a una subfórmula enterrada dentro de un antecedente complejo, los postulados de display reescriben la estructura circundante para que esa subfórmula aparezca sola a la izquierda del símbolo de juicio; la regla de implicación se aplica directamente y el sequent se reordena según haga falta, haciendo el procedimiento sistemático para todos los conectivos.

Aplicación incorrecta

Suponer que la lógica de display simplifica automáticamente cualquier prueba o ignorar el coste de reordenamientos estructurales repetidos puede ser engañoso: el uso ingenuo puede ocultar complejidad, y aplicar postulados de display sin garantizar la admisibilidad de reglas estructurales para la lógica objetivo puede producir extensiones incorrectas o no conservativas.

Consecuencia

La lógica de display ofrece un tratamiento uniforme y modular de muchos conectivos y reglas estructurales, a menudo simplificando pruebas meta-teóricas (eliminación de cortes, conservatividad) y permitiendo transferir conocimientos estructurales entre lógicas que comparten estructura exhibible.

Inversión

Lo contrario es trabajar sin exhibibilidad, usando cálculos sequent donde las subestructuras no siempre pueden aislarse mediante postulados generales; tales cálculos pueden ser más sencillos de implementar en algunos casos pero pierden el mecanismo uniforme para gestionar contextos estructurales arbitrarios.

Límite

La lógica de display se aplica cuando se pueden definir conectivos estructurales y postulados para mover subestructuras; puede no aportar ventajas para lógicas cuyo comportamiento estructural resista a los postulados de display o cuando el coste de la manipulación estructural supere la ganancia en uniformidad.

Tensión semántica

Tensión entre la lógica de display y otros cálculos estructurales (sequent, hypersequent, sistemas etiquetados): la lógica de display enfatiza un álgebra estructural universal y postulados para aislar subestructuras, mientras que las alternativas compensan la generalidad por una sintaxis más simple o representaciones semánticas más directas.

Síntesis

La Lógica de Display ofrece un álgebra estructural y postulados de display que hacen accesible cualquier subestructura para la aplicación de reglas: reordenando sistemáticamente los sequents hasta la forma de exhibición se obtiene un tratamiento uniforme de conectivos y estructuras que facilita una metateoría modular, a costa de una contabilidad estructural explícita.