Cálculo de secuentes de la lógica Semi-intuicionista

JUAN MANUEL CORNEJO; DIEGO CASTAÑO

Bahía Blanca

Congreso; XIII Congreso Dr. Antonio Monteiro; 2015

Universidad Nacional del Sur

La variedad $mathcal{SH}$ de las ´algebras de semi-Heyting fue introducida por Sankappanavar en cite{sankappanavar2008semi} como una abstracci´on de la variedad de las ´algebras de Heyting. Un ´algebra de semi-Heyting es un ´algebra de la forma $mathbb{L} = langle L,ee, wedge, ightarrow, 0, 1 angle$ tal que $langle L, ee, wedge, 0, 1 angle$ es un reticulado con 0 y 1 %satisfacen las siguientes condiciones: %egin{enumerate} %item[(a)]$x wedge (x ightarrow y) approx x wedge y$, %item[(b)]$x wedge (y ightarrow z) %approx x wedge [(x wedge y) ightarrow (x wedge z)]$, %item[(c)]$x % ightarrow x approx 1$. %end{enumerate} y en la que se satisfacen las identidades: $x wedge (x ightarrow y) approx x wedge y, x wedge (y ightarrow z) approx x wedge [(x wedge y) ightarrow (x wedge z)]$ y $x ightarrow x approx 1$ Esta variedad incluye las álgebras de Heyting y comparten algunas propiedades importantes. Por ejemplo, la variedad de las álgebras de semi-Heyting es aritmética, las álgebras de semi-Heyting son reticulados distributivos pseudocomplementados, con el pseudocomplemento dado por $x^{*} = x ightarrow 0$, y sus congruencias están determinadas por filtros de reticulado. Pero, al mismo tiempo, las álgebras de semi-Heyting presentan diferencias bien remarcadas. La implicación sobre un álgebra de semi-Heyting ${mathbf A}$ no está determinada por el orden del reticulado de ${mathbf A}$. En los últimos años la variedad $mathcal{SH}$, subvariedades y expansiones han sido estudiadas desde un enfoque algebraico, por ejmplo, en cite{Abad2010variety,Abad2012glivenko,Abad2013semi,sankappanavar2011expansions}. Es sabido que las álgebras de Heyting constituyen una semántica algebraica de la lógica intuicionista. A su vez las álgebras de semi-Heyting están asociadas a una lógica, $mathcal{SI}$, denominada {it Lógica semi-intuicionista} que fue introducida en cite{cornejo2011semi} al estilo Hilbert. Algunos aspectos relacionados a $mathcal{SI}$ han sido estudiados en cite{cornejo14semiLogics,cornejo2014semi}. El principal objetivo de este trabajo es el de introducir y estudiar un cálculo de secuentes estilo Gentzen para la lógica $mathcal{SI}$, basado en el cálculo de secuentes del intuicionismo cite{galatos2007residuated}, que tiene como propiedades principales la decidiblidad, la admisión de la regla de corte y la completitud respecto de $mathcal{SH}$. Consecuentemente proporciona un algoritmo para determinar, en una cantidad finita de pasos, si una identidad es válida o no en la clase de las álgebras de semi-Heyting.