Sobre reglas multiarias en teoría de la prueba

Ponente(s): Favio Ezequiel Miranda Perea

En la teoría estructural de la prueba, una regla es multiaria si permite introducir múltiples instancias de un conectivo, por ejemplo $A_1\to A_2\to \ldots \to A_n\to B$ en vez de únicamente $A\to B$, o bien más de un operador lógico, digamos $\forall \vec{x}(A\to \fa\vec{y}B)$, en lugar de introducir esta fórmula con aplicaciones iteradas de las reglas unitarias para el condicional y el cuantificador universal. Desde el punto de vista de la semántica constructiva estos esquemas de inferencia pueden considerarse como defectuosos puesto que las reglas se utilizan para dar significado a los operadores lógicos y por lo tanto no deben involucrar a más de una operación lógica. Sin embargo, desde el punto de vista de la práctica matemática, las reglas multiarias resultan útiles para capturar patrones comunes de razonamiento. En esta charla discutimos una regla multiaria para la implicación y el cuantificador universal; su equivalencia con el cálculo de secuentes usual; su estrecha relación con la regla de corte (uso de lemas); y sus ventajas sobre las reglas usuales para el condicional y el cuantificador universal. Este trabajo recibe apoyo del proyecto UNAM-DGAPA-PAPIIT IN101723